1 /-
2 Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Sébastien Gouëzel
5 -/
6
7 import topology.topological_fiber_bundle geometry.manifold.smooth_manifold_with_corners
src └───────────────────────────────┘ └────────────────────────────────────────────┘
8 /-!
9 # Basic smooth bundles
10
11 In general, a smooth bundle is a bundle over a smooth manifold, whose fiber is a manifold, and
12 for which the coordinate changes are smooth. In this definition, there are charts involved at
13 several places: in the manifold structure of the base, in the manifold structure of the fibers, and
14 in the local trivializations. This makes it a complicated object in general. There is however a
15 specific situation where things are much simpler: when the fiber is a vector space (no need for
16 charts for the fibers), and when the local trivializations of the bundle and the charts of the base
17 coincide. Then everything is expressed in terms of the charts of the base, making for a much
18 simpler overall structure, which is easier to manipulate formally.
19
20 Most vector bundles that naturally occur in differential geometry are of this form:
21 the tangent bundle, the cotangent bundle, differential forms (used to define de Rham cohomology)
22 and the bundle of Riemannian metrics. Therefore, it is worth defining a specific constructor for
23 this kind of bundle, that we call basic smooth bundles.
24
25 A basic smooth bundle is thus a smooth bundle over a smooth manifold whose fiber is a vector space,
26 and which is trivial in the coordinate charts of the base. (We recall that in our notion of manifold
27 there is a distinguished atlas, which does not need to be maximal: we require the triviality above
28 this specific atlas). It can be constructed from a basic smooth bundled core, defined below,
29 specifying the changes in the fiber when one goes from one coordinate chart to another one. We do
30 not require that this changes in fiber are linear, but only diffeomorphisms.
31
32 ## Main definitions
33
34 * `basic_smooth_bundle_core I M F`: assuming that `M` is a smooth manifold over the model with
35 corners `I` on `(𝕜, E, H)`, and `F` is a normed vector space over `𝕜`, this structure registers,
36 for each pair of charts of `M`, a smooth change of coordinates on `F`. This is the core structure
37 from which one will build a smooth bundle with fiber `F` over `M`.
38
39 Let `Z` be a basic smooth bundle core over `M` with fiber `F`. We define
40 `Z.to_topological_fiber_bundle_core`, the (topological) fiber bundle core associated to `Z`. From it,
41 we get a space `Z.to_topological_fiber_bundle_core.total_space` (which as a Type is just `M × F`),
42 with the fiber bundle topology. It inherits a manifold structure (where the charts are in bijection
43 with the charts of the basis). We show that this manifold is smooth.
44
45 Then we use this machinery to construct the tangent bundle of a smooth manifold.
46
47 * `tangent_bundle_core I M`: the basic smooth bundle core associated to a smooth manifold `M` over a
48 model with corners `I`.
49 * `tangent_bundle I M` : the total space of `tangent_bundle_core I M`. It is itself a
50 smooth manifold over the model with corners `I.tangent`, the product of `I` and the trivial model
51 with corners on `E`.
52 * `tangent_space I x` : the tangent space to `M` at `x`
53 * `tangent_bundle.proj I M`: the projection from the tangent bundle to the base manifold
54
55 ## Implementation notes
56
57 In the definition of a basic smooth bundle core, we do not require that the coordinate changes of
58 the fibers are linear map, only that they are diffeomorphisms. Therefore, the fibers of the
59 resulting fiber bundle do not inherit a vector space structure (as an algebraic object) in general.
60 As the fiber, as a type, is just `F`, one can still always register the vector space structure, but
61 it does not make sense to do so (i.e., it will not lead to any useful theorem) unless this structure
62 is canonical, i.e., the coordinate changes are linear maps.
63
64 For instance, we register the vector space structure on the fibers of the tangent bundle. However,
65 we do not register the normed space structure coming from that of `F` (as it is not canonical, and
66 we also want to keep the possibility to add a Riemannian structure on the manifold later on without
67 having two competing normed space instances on the tangent spaces).
68
69 We require `F` to be a normed space, and not just a topological vector space, as we want to talk
70 about smooth functions on `F`. The notion of derivative requires a norm to be defined.
71
72 ## TODO
73 construct the cotangent bundle, and the bundles of differential forms. They should follow
74 functorially from the description of the tangent bundle as a basic smooth bundle.
75
76 ## Tags
77 Smooth fiber bundle, vector bundle, tangent space, tangent bundle
78 -/
79
80 noncomputable theory
81
82 universe u
83
84 open topological_space set
85
86 /-- Core structure used to create a smooth bundle above `M` (a manifold over the model with
87 corner `I`) with fiber the normed vector space `F` over `𝕜`, which is trivial in the chart domains
88 of `M`. This structure registers the changes in the fibers when one changes coordinate charts in the
89 base. We do not require the change of coordinates of the fibers to be linear, only smooth.
90 Therefore, the fibers of the resulting bundle will not inherit a canonical vector space structure
91 in general. -/
92 structure basic_smooth_bundle_core {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
id └───┘ └──────────────────────┘ ┴
src └──────────────────────┘
typ └───┘ └──────────────────────┘ ┴
doc └──────────────────────┘
93 {E : Type u} [normed_group E] [normed_space 𝕜 E]
id └──┘ └──────────┘ ┴ └──────────┘ ┴ ┴
src └──────────┘ └──────────┘
typ └──┘ └──────────┘ ┴ └──────────┘ ┴ ┴
doc └──────────┘ └──────────┘
94 {H : Type*} [topological_space H] (I : model_with_corners 𝕜 E H)
id └───┘ └───────────────┘ ┴ └────────────────┘ ┴ ┴ ┴
src └───────────────┘ └────────────────┘
typ └───┘ └───────────────┘ ┴ └────────────────┘ ┴ ┴ ┴
doc └───────────────┘ └────────────────┘
95 (M : Type*) [topological_space M] [manifold H M] [smooth_manifold_with_corners I M]
id └───┘ └───────────────┘ ┴ └──────┘ ┴ ┴ └──────────────────────────┘ ┴ ┴
src └───────────────┘ └──────┘ └──────────────────────────┘
typ └───┘ └───────────────┘ ┴ └──────┘ ┴ ┴ └──────────────────────────┘ ┴ ┴
doc └───────────────┘ └──────┘ └──────────────────────────┘
96 (F : Type u) [normed_group F] [normed_space 𝕜 F] :=
id └──┘ └──────────┘ ┴ └──────────┘ ┴ ┴
src └──────────┘ └──────────┘
typ └──┘ └──────────┘ ┴ └──────────┘ ┴ ┴
doc └──────────┘ └──────────┘
97 (coord_change : atlas H M → atlas H M → H → F → F)
id └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴
src └───┘ └───┘
typ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴
98 (coord_change_self :
99 ∀ i : atlas H M, ∀ x ∈ i.1.target, ∀ v, coord_change i i x v = v)
id ┴ └───┘ ┴ ┴ ┴ ┴┴ └────┘ ┴ └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └───┘ ┴ ┴ └────┘ ┴
typ ┴ └───┘ ┴ ┴ ┴ ┴┴ └────┘ ┴ └──────────┘ ┴ ┴ ┴ ┴ ┴ ┴
100 (coord_change_comp : ∀ i j k : atlas H M,
id ┴ └───┘ ┴ ┴
src └───┘
typ ┴ └───┘ ┴ ┴
101 ∀ x ∈ ((i.1.symm.trans j.1).trans (j.1.symm.trans k.1)).source, ∀ v,
id ┴ ┴┴ └──┘ └───┘ ┴┴ └───┘ ┴┴ └──┘ └───┘ ┴┴ └────┘ ┴
src ┴ └──┘ └───┘ ┴ └───┘ ┴ └──┘ └───┘ ┴ └────┘
typ ┴ ┴┴ └──┘ └───┘ ┴┴ └───┘ ┴┴ └──┘ └───┘ ┴┴ └────┘ ┴
doc └──┘ └───┘ └───┘ └──┘ └───┘
102 (coord_change j k ((i.1.symm.trans j.1).to_fun x)) (coord_change i j x v) = coord_change i k x v)
id └──────────┘ ┴ ┴ ┴┴ └──┘ └───┘ ┴┴ └────┘ ┴ └──────────┘ ┴ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴
src ┴ └──┘ └───┘ ┴ └────┘ ┴
typ └──────────┘ ┴ ┴ ┴┴ └──┘ └───┘ ┴┴ └────┘ ┴ └──────────┘ ┴ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴
doc └──┘ └───┘
103 (coord_change_smooth : ∀ i j : atlas H M,
id ┴ └───┘ ┴ ┴
src └───┘
typ ┴ └───┘ ┴ ┴
104 times_cont_diff_on 𝕜 ⊤ (λp : E × F, coord_change i j (I.inv_fun p.1) p.2)
id └────────────────┘ ┴ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴└──────┘ ┴┴ ┴┴
src └────────────────┘ ┴ ┴ └──────┘ ┴ ┴
typ └────────────────┘ ┴ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴└──────┘ ┴┴ ┴┴
doc └────────────────┘
105 ((I.to_fun '' (i.1.symm.trans j.1).source).prod (univ : set F)))
id ┴└─────┘ └┘ ┴┴ └──┘ └───┘ ┴┴ └────┘ └──┘ └──┘ └─┘ ┴
src └─────┘ └┘ ┴ └──┘ └───┘ ┴ └────┘ └──┘ └──┘ └─┘
typ ┴└─────┘ └┘ ┴┴ └──┘ └───┘ ┴┴ └────┘ └──┘ └──┘ └─┘ ┴
doc └──┘ └───┘ └──┘
106
107 namespace basic_smooth_bundle_core
108
109 variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
id └──────────────────────┘
src └──────────────────────┘
typ └──────────────────────┘
doc └──────────────────────┘
110 {E : Type u} [normed_group E] [normed_space 𝕜 E]
id └──────────┘ └──────────┘
src └──────────┘ └──────────┘
typ └──────────┘ └──────────┘
doc └──────────┘ └──────────┘
111 {H : Type*} [topological_space H] {I : model_with_corners 𝕜 E H}
id └───────────────┘ └────────────────┘
src └───────────────┘ └────────────────┘
typ └───────────────┘ └────────────────┘
doc └───────────────┘ └────────────────┘
112 {M : Type*} [topological_space M] [manifold H M] [smooth_manifold_with_corners I M]
id └───────────────┘ └──────┘ └──────────────────────────┘
src └───────────────┘ └──────┘ └──────────────────────────┘
typ └───────────────┘ └──────┘ └──────────────────────────┘
doc └───────────────┘ └──────┘ └──────────────────────────┘
113 {F : Type u} [normed_group F] [normed_space 𝕜 F]
id └──────────┘ └──────────┘
src └──────────┘ └──────────┘
typ └──────────┘ └──────────┘
doc └──────────┘ └──────────┘
114 (Z : basic_smooth_bundle_core I M F)
id └──────────────────────┘
src └──────────────────────┘
typ └──────────────────────┘
doc └──────────────────────┘
115
116 /-- Fiber bundle core associated to a basic smooth bundle core -/
117 def to_topological_fiber_bundle_core : topological_fiber_bundle_core (atlas H M) M F :=
id └───────────────────────────┘ └───┘ ┴ ┴ ┴ ┴
src └───────────────────────────┘ └───┘
typ └───────────────────────────┘ └───┘ ┴ ┴ ┴ ┴
doc └───────────────────────────┘
118 { base_set := λi, i.1.source,
id ┴ ┴┴ └────┘
src ┴ └────┘
typ ┴ ┴┴ └────┘
119 is_open_base_set := λi, i.1.open_source,
id ┴ ┴┴ └─────────┘
src ┴ └─────────┘
typ ┴ ┴┴ └─────────┘
120 index_at := λx, ⟨chart_at H x, chart_mem_atlas H x⟩,
id ┴ └──────┘ ┴ ┴ └─────────────┘ ┴ ┴
src └──────┘ └─────────────┘
typ ┴ └──────┘ ┴ ┴ └─────────────┘ ┴ ┴
121 mem_base_set_at := λx, mem_chart_source H x,
id ┴ └──────────────┘ ┴ ┴
src └──────────────┘
typ ┴ └──────────────┘ ┴ ┴
122 coord_change := λi j x v, Z.coord_change i j (i.1.to_fun x) v,
id ┴ ┴ ┴ ┴ ┴└───────────┘ ┴ ┴ ┴┴ └────┘ ┴ ┴
src └───────────┘ ┴ └────┘
typ ┴ ┴ ┴ ┴ ┴└───────────┘ ┴ ┴ ┴┴ └────┘ ┴ ┴
123 coord_change_self := λi x hx v, Z.coord_change_self i (i.1.to_fun x) (i.1.map_source hx) v,
id ┴ ┴ └┘ ┴ ┴└────────────────┘ ┴ ┴┴ └────┘ ┴ ┴┴ └────────┘ └┘ ┴
src └────────────────┘ ┴ └────┘ ┴ └────────┘
typ ┴ ┴ └┘ ┴ ┴└────────────────┘ ┴ ┴┴ └────┘ ┴ ┴┴ └────────┘ └┘ ┴
124 coord_change_comp := λi j k x ⟨⟨hx1, hx2⟩, hx3⟩ v, begin
id ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
st └─────
125 have := Z.coord_change_comp i j k (i.1.to_fun x) _ v,
id └─────────────────┘ ┴ ┴ ┴ ┴ ┴
src └──────┘└─────────────────┘┴ ┴ ┴ ┴ └────────┘ └──┘
typ └──────┘└─────────────────┘┴ ┴┴┴┴┴ ┴└────────┘┴└──┘┴
doc └──────┘ ┴ ┴ ┴ ┴ └────────┘ └──┘
txt └──────┘ ┴ ┴ ┴ ┴ └────────┘ └──┘
par └──────┘ ┴ ┴ ┴ ┴ └────────┘ └──┘
pid └───┘└─┘ ┴ ┴ ┴ ┴ └────────┘ └──┘
st ───────────────────────────────────────────────────────┘└─
126 convert this using 2,
id └──┘
src └──────┘ └──────┘
typ └──────┘└──┘└──────┘
doc └──────┘ └──────┘
txt └──────┘ └──────┘
par └──────┘ └──────┘
pid ┴ └─────┘┴
st ───────────────────────┘└─
127 { simp [hx1] },
id └─┘
src └────┘ └┘
typ └────┘└─┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴┴ ┴┴
st ─────┘└─────────┘└┘└
128 { simp [local_equiv.trans_source, hx1, hx2, hx3, i.1.map_source, j.1.map_source] }
id └──────────────────────┘ └─┘ └─┘ └─┘ ┴ ┴
src └────┘└──────────────────────┘└┘ └┘ └┘ └┘ └─────────────┘ └─────────────┘
typ └────┘└──────────────────────┘└┘└─┘└┘└─┘└┘└─┘└┘┴└─────────────┘┴└─────────────┘
doc └────┘ └┘ └┘ └┘ └┘ └─────────────┘ └─────────────┘
txt └────┘ └┘ └┘ └┘ └┘ └─────────────┘ └─────────────┘
par └────┘ └┘ └┘ └┘ └┘ └─────────────┘ └─────────────┘
pid ┴┴ └┘ └┘ └┘ └┘ └─────────────┘ └────────────┘┴
st ────────────────────────────────────────────────────────────────────────────────────┘└─
129 end,
st ────┘
130 coord_change_continuous := λi j, begin
id ┴ ┴
typ ┴ ┴
st └─────
131 have A : continuous_on (λp : E × F, Z.coord_change i j (I.inv_fun p.1) p.2)
id └───────────┘ ┴ ┴ └────────────┘ └───────┘
src └───────┘└───────────┘┴ └──┘ ┴┴┴ └┘└────────────┘┴ ┴ ┴ └───────┘┴ └──┘ └───
typ └───────┘└───────────┘┴ └──┘┴┴┴┴ └┘└────────────┘┴ ┴ ┴ └───────┘┴ └──┘ └───
doc └───────┘└───────────┘┴ └──┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──┘ └───
txt └───────┘ ┴ └──┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──┘ └───
par └───────┘ ┴ └──┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──┘ └───
pid └────┘└─┘ ┴ └──┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──┘ └───
st ────────────────────────────────────────────────────────────────────────────────
132 ((I.to_fun '' (i.1.symm.trans j.1).source).prod (univ : set F)) :=
id └──────┘ └┘ ┴ ┴ └──┘ └─┘ ┴
src ─────┘ └──────┘┴└┘┴ └────────────┘ └───────────────┘ └──┘└─┘└─┘┴ └─────
typ ─────┘ └──────┘┴└┘┴ ┴└────────────┘┴└───────────────┘ └──┘└─┘└─┘┴┴└─────
doc ─────┘ ┴ ┴ └────────────┘ └───────────────┘ └─┘ ┴ └─────
txt ─────┘ ┴ ┴ └────────────┘ └───────────────┘ └─┘ ┴ └─────
par ─────┘ ┴ ┴ └────────────┘ └───────────────┘ └─┘ ┴ └─────
pid ─────┘ ┴ ┴ └────────────┘ └───────────────┘ └─┘ ┴ └┘└───
st ─────────────────────────────────────────────────────────────────────────
133 (Z.coord_change_smooth i j).continuous_on,
id └───────────────────┘ ┴ ┴
src ─────┘ └───────────────────┘┴ ┴ └─────────────┘
typ ─────┘ └───────────────────┘┴┴┴┴└─────────────┘
doc ─────┘ ┴ ┴ └─────────────┘
txt ─────┘ ┴ ┴ └─────────────┘
par ─────┘ ┴ ┴ └─────────────┘
pid ─────┘ ┴ ┴ └────────────┘┴
st ──────────────────────────────────────────────┘└─
134 have B : continuous_on (λx : M, I.to_fun (i.1.to_fun x)) i.1.source :=
id └───────────┘ ┴ └──────┘ ┴
src └───────┘└───────────┘┴ └──┘ └┘└──────┘┴ └────────┘ └─┘ └────────────
typ └───────┘└───────────┘┴ └──┘┴└┘└──────┘┴ └────────┘ └─┘┴└────────────
doc └───────┘└───────────┘┴ └──┘ └┘ ┴ └────────┘ └─┘ └────────────
txt └───────┘ ┴ └──┘ └┘ ┴ └────────┘ └─┘ └────────────
par └───────┘ ┴ └──┘ └┘ ┴ └────────┘ └─┘ └────────────
pid └────┘└─┘ ┴ └──┘ └┘ ┴ └────────┘ └─┘ └──────┘└────
st ───────────────────────────────────────────────────────────────────────────
135 I.continuous_to_fun.comp_continuous_on i.1.continuous_to_fun,
id └────────────────────────────────────┘ ┴
src ─────┘└────────────────────────────────────┘┴ └──────────────────┘
typ ─────┘└────────────────────────────────────┘┴┴└──────────────────┘
doc ─────┘ ┴ └──────────────────┘
txt ─────┘ ┴ └──────────────────┘
par ─────┘ ┴ └──────────────────┘
pid ─────┘ ┴ └─────────────────┘┴
st ─────────────────────────────────────────────────────────────────┘└─
136 have C : continuous_on (λp : M × F, (⟨I.to_fun (i.1.to_fun p.1), p.2⟩ : E × F))
id └───────────┘ ┴ ┴ └──────┘ ┴ ┴
src └───────┘└───────────┘┴ └──┘ ┴ ┴ └┘ └──────┘┴ └────────┘ └───┘ └────┘ ┴ ┴ └──
typ └───────┘└───────────┘┴ └──┘┴┴┴┴ └┘ └──────┘┴ └────────┘ └───┘ └────┘┴┴ ┴┴└──
doc └───────┘└───────────┘┴ └──┘ ┴ ┴ └┘ ┴ └────────┘ └───┘ └────┘ ┴ ┴ └──
txt └───────┘ ┴ └──┘ ┴ ┴ └┘ ┴ └────────┘ └───┘ └────┘ ┴ ┴ └──
par └───────┘ ┴ └──┘ ┴ ┴ └┘ ┴ └────────┘ └───┘ └────┘ ┴ ┴ └──
pid └────┘└─┘ ┴ └──┘ ┴ ┴ └┘ ┴ └────────┘ └───┘ └────┘ ┴ ┴ └──
st ────────────────────────────────────────────────────────────────────────────────────
137 (i.1.source.prod univ),
id ┴ └──┘
src ────────────┘ └─────────────┘└──┘┴
typ ────────────┘ ┴└─────────────┘└──┘┴
doc ────────────┘ └─────────────┘ ┴
txt ────────────┘ └─────────────┘ ┴
par ────────────┘ └─────────────┘ ┴
pid ────────────┘ └─────────────┘ ┴
st ──────────────────────────────────┘└─
138 { apply continuous_on.prod _ continuous_snd.continuous_on,
id └────────────────┘ └──────────────────────────┘
src └────┘└────────────────┘└─┘└──────────────────────────┘
typ └────┘└────────────────┘└─┘└──────────────────────────┘
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ └─┘
st ─────┘└─────────────────────────────────────────────────────┘└─
139 exact B.comp continuous_fst.continuous_on (prod_subset_preimage_fst _ _) },
id └────┘ └──────────────────────────┘ └──────────────────────┘
src └────┘└────┘┴└──────────────────────────┘┴ └──────────────────────┘└────┘
typ └────┘└────┘┴└──────────────────────────┘┴ └──────────────────────┘└────┘
doc └────┘ ┴ ┴ └────┘
txt └────┘ ┴ ┴ └────┘
par └────┘ ┴ ┴ └────┘
pid ┴ ┴ ┴ └───┘┴
st ──────────────────────────────────────────────────────────────────────────────┘└┘└
140 have C' : continuous_on (λp : M × F, (⟨I.to_fun (i.1.to_fun p.1), p.2⟩ : E × F))
id └───────────┘ ┴ └──────┘ ┴ ┴
src └────────┘└───────────┘┴ └──┘ ┴ ┴ └┘ └──────┘┴ └────────┘ └───┘ └────┘ ┴ ┴ └──
typ └────────┘└───────────┘┴ └──┘┴┴ ┴ └┘ └──────┘┴ └────────┘ └───┘ └────┘┴┴ ┴┴└──
doc └────────┘└───────────┘┴ └──┘ ┴ ┴ └┘ ┴ └────────┘ └───┘ └────┘ ┴ ┴ └──
txt └────────┘ ┴ └──┘ ┴ ┴ └┘ ┴ └────────┘ └───┘ └────┘ ┴ ┴ └──
par └────────┘ ┴ └──┘ ┴ ┴ └┘ ┴ └────────┘ └───┘ └────┘ ┴ ┴ └──
pid └─────┘└─┘ ┴ └──┘ ┴ ┴ └┘ ┴ └────────┘ └───┘ └────┘ ┴ ┴ └──
st ─────────────────────────────────────────────────────────────────────────────────────
141 ((i.1.source ∩ j.1.source).prod univ) :=
id ┴ ┴ ┴ └──┘
src ─────────────┘ └────────┘┴┴ └──────────────┘└──┘└────
typ ─────────────┘ ┴└────────┘┴┴┴└──────────────┘└──┘└────
doc ─────────────┘ └────────┘ ┴ └──────────────┘ └────
txt ─────────────┘ └────────┘ ┴ └──────────────┘ └────
par ─────────────┘ └────────┘ ┴ └──────────────┘ └────
pid ─────────────┘ └────────┘ ┴ └──────────────┘ ┴└───
st ───────────────────────────────────────────────────────
142 continuous_on.mono C (prod_mono (inter_subset_left _ _) (subset.refl _)),
id └────────────────┘ ┴ └───────┘ └───────────────┘ └─────────┘
src ─────┘└────────────────┘┴ ┴ └───────┘┴ └───────────────┘└────┘ └─────────┘└──┘
typ ─────┘└────────────────┘┴┴┴ └───────┘┴ └───────────────┘└────┘ └─────────┘└──┘
doc ─────┘ ┴ ┴ ┴ └────┘ └──┘
txt ─────┘ ┴ ┴ ┴ └────┘ └──┘
par ─────┘ ┴ ┴ ┴ └────┘ └──┘
pid ─────┘ ┴ ┴ ┴ └────┘ └──┘
st ─────────────────────────────────────────────────────────────────────────────┘└─
143 have D : (i.1.source ∩ j.1.source).prod univ ⊆ (λ (p : M × F),
id ┴ ┴ ┴
src └───────┘ └────────┘ ┴ └──────────────┘ ┴┴┴ └────┘ ┴ ┴ └──
typ └───────┘ └────────┘ ┴ └──────────────┘ ┴┴┴ └────┘┴┴ ┴┴└──
doc └───────┘ └────────┘ ┴ └──────────────┘ ┴ ┴ └────┘ ┴ ┴ └──
txt └───────┘ └────────┘ ┴ └──────────────┘ ┴ ┴ └────┘ ┴ ┴ └──
par └───────┘ └────────┘ ┴ └──────────────┘ ┴ ┴ └────┘ ┴ ┴ └──
pid └────┘└─┘ └────────┘ ┴ └──────────────┘ ┴ ┴ └────┘ ┴ ┴ └──
st ───────────────────────────────────────────────────────────────────
144 (I.to_fun (i.1.to_fun p.1), p.2)) ⁻¹' ((I.to_fun '' (i.1.symm.trans j.1).source).prod univ),
id ┴ └─┘ └──────┘ ┴ ┴ └──┘
src ─────┘┴ ┴ └────────┘ └───┘ └───┘└─┘┴ └──────┘┴ ┴ └────────────┘ └───────────────┘└──┘┴
typ ─────┘┴ ┴ └────────┘ └───┘ └───┘└─┘┴ └──────┘┴ ┴ ┴└────────────┘┴└───────────────┘└──┘┴
doc ─────┘ ┴ └────────┘ └───┘ └───┘└─┘┴ ┴ ┴ └────────────┘ └───────────────┘ ┴
txt ─────┘ ┴ └────────┘ └───┘ └───┘ ┴ ┴ ┴ └────────────┘ └───────────────┘ ┴
par ─────┘ ┴ └────────┘ └───┘ └───┘ ┴ ┴ ┴ └────────────┘ └───────────────┘ ┴
pid ─────┘ ┴ └────────┘ └───┘ └───┘ ┴ ┴ ┴ └────────────┘ └───────────────┘ ┴
st ────────────────────────────────────────────────────────────────────────────────────────────────┘└─
145 { rintros ⟨x, v⟩ hx,
src └───────────────┘
typ └───────────────┘
doc └───────────────┘
txt └───────────────┘
par └───────────────┘
pid └────────┘
st ─────┘└───────────────┘└─
146 simp at hx,
src └────────┘
typ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
pid ┴└───┘
st ───────────────┘└─
147 simp [mem_image_of_mem, local_equiv.trans_source, hx] },
id └──────────────┘ └──────────────────────┘ └┘
src └────┘└──────────────┘└┘└──────────────────────┘└┘ └┘
typ └────┘└──────────────┘└┘└──────────────────────┘└┘└┘└┘
doc └────┘ └┘ └┘ └┘
txt └────┘ └┘ └┘ └┘
par └────┘ └┘ └┘ └┘
pid ┴┴ └┘ └┘ ┴┴
st ───────────────────────────────────────────────────────────┘└┘└
148 convert continuous_on.comp A C' D,
id └────────────────┘ ┴ └┘ ┴
src └──────┘└────────────────┘┴ ┴ ┴
typ └──────┘└────────────────┘┴┴┴└┘┴┴
doc └──────┘ ┴ ┴ ┴
txt └──────┘ ┴ ┴ ┴
par └──────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ────────────────────────────────────┘└─
149 ext p,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid └┘
st ────────┘└─
150 simp
src └────
typ └────
doc └────
txt └────
par └────
pid └
st ─────────
151 end }
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
152
153 @[simp] lemma base_set (i : atlas H M) :
id └───┘ ┴ ┴
src └───┘
typ └───┘ ┴ ┴
doc └──┘
154 Z.to_topological_fiber_bundle_core.base_set i = i.1.source := rfl
id ┴└───────────────────────────────┘└───────┘ ┴ ┴ ┴┴ └────┘ └─┘
src └───────────────────────────────┘└───────┘ ┴ ┴ └────┘ └─┘
typ ┴└───────────────────────────────┘└───────┘ ┴ ┴ ┴┴ └────┘ └─┘
doc └───────────────────────────────┘
155
156 /-- Local chart for the total space of a basic smooth bundle -/
157 def chart {e : local_homeomorph M H} (he : e ∈ atlas H M) :
id └──────────────┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴
src └──────────────┘ ┴ └───┘
typ └──────────────┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴
doc └──────────────┘
158 local_homeomorph (Z.to_topological_fiber_bundle_core.total_space) (H × F) :=
id └──────────────┘ ┴└───────────────────────────────┘└──────────┘ ┴ ┴ ┴
src └──────────────┘ └───────────────────────────────┘└──────────┘ ┴
typ └──────────────┘ ┴└───────────────────────────────┘└──────────┘ ┴ ┴ ┴
doc └──────────────┘ └───────────────────────────────┘└──────────┘
159 (Z.to_topological_fiber_bundle_core.local_triv ⟨e, he⟩).trans
id ┴└───────────────────────────────┘└─────────┘ ┴ └┘ └───┘
src └───────────────────────────────┘└─────────┘ └───┘
typ ┴└───────────────────────────────┘└─────────┘ ┴ └┘ └───┘
doc └───────────────────────────────┘└─────────┘ └───┘
160 (local_homeomorph.prod e (local_homeomorph.refl F))
id └───────────────────┘ ┴ └───────────────────┘ ┴
src └───────────────────┘ └───────────────────┘
typ └───────────────────┘ ┴ └───────────────────┘ ┴
doc └───────────────────┘ └───────────────────┘
161
162 @[simp] lemma chart_source (e : local_homeomorph M H) (he : e ∈ atlas H M) :
id └──────────────┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴
src └──────────────┘ ┴ └───┘
typ └──────────────┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴
doc └──┘ └──────────────┘
163 (Z.chart he).source = Z.to_topological_fiber_bundle_core.proj ⁻¹' e.source :=
id ┴└────┘ └┘ └────┘ ┴ ┴└───────────────────────────────┘└───┘ └─┘ ┴└─────┘
src └────┘ └────┘ ┴ └───────────────────────────────┘└───┘ └─┘ └─────┘
typ ┴└────┘ └┘ └────┘ ┴ ┴└───────────────────────────────┘└───┘ └─┘ ┴└─────┘
doc └────┘ └───────────────────────────────┘└───┘ └─┘
164 by { ext p, simp [chart, local_equiv.trans_source] }
id └───┘ └──────────────────────┘
src └───┘ └────┘└───┘└┘└──────────────────────┘└┘
typ └───┘ └────┘└───┘└┘└──────────────────────┘└┘
doc └───┘ └────┘└───┘└┘ └┘
txt └───┘ └────┘ └┘ └┘
par └───┘ └────┘ └┘ └┘
pid └┘ ┴┴ └┘ ┴┴
st └──────┘└───────────────────────────────────────┘└┘
165
166 @[simp] lemma chart_target (e : local_homeomorph M H) (he : e ∈ atlas H M) :
id └──────────────┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴
src └──────────────┘ ┴ └───┘
typ └──────────────┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴
doc └──┘ └──────────────┘
167 (Z.chart he).target = e.target.prod univ :=
id ┴└────┘ └┘ └────┘ ┴ ┴└─────┘└───┘ └──┘
src └────┘ └────┘ ┴ └─────┘└───┘ └──┘
typ ┴└────┘ └┘ └────┘ ┴ ┴└─────┘└───┘ └──┘
doc └────┘ └───┘
168 begin
st └─────
169 simp only [chart, local_equiv.trans_target, local_homeomorph.prod_to_local_equiv, id.def,
id └───┘ └──────────────────────┘ └──────────────────────────────────┘ └────┘
src └─────────┘└───┘└┘└──────────────────────┘└┘└──────────────────────────────────┘└┘└────┘└─
typ └─────────┘└───┘└┘└──────────────────────┘└┘└──────────────────────────────────┘└┘└────┘└─
doc └─────────┘└───┘└┘ └┘ └┘ └─
txt └─────────┘ └┘ └┘ └┘ └─
par └─────────┘ └┘ └┘ └┘ └─
pid ┴└──┘└┘ └┘ └┘ └┘ └─
st ────────────────────────────────────────────────────────────────────────────────────────────
170 local_equiv.refl_inv_fun, local_homeomorph.trans_to_local_equiv, local_equiv.refl_target,
id └──────────────────────┘ └───────────────────────────────────┘ └─────────────────────┘
src ───────┘└──────────────────────┘└┘└───────────────────────────────────┘└┘└─────────────────────┘└─
typ ───────┘└──────────────────────┘└┘└───────────────────────────────────┘└┘└─────────────────────┘└─
doc ───────┘ └┘ └┘ └─
txt ───────┘ └┘ └┘ └─
par ───────┘ └┘ └┘ └─
pid ───────┘ └┘ └┘ └─
st ──────────────────────────────────────────────────────────────────────────────────────────────────
171 local_homeomorph.refl_local_equiv, local_equiv.prod_target, local_homeomorph.prod_inv_fun],
id └───────────────────────────────┘ └─────────────────────┘ └───────────────────────────┘
src ───────┘└───────────────────────────────┘└┘└─────────────────────┘└┘└───────────────────────────┘┴
typ ───────┘└───────────────────────────────┘└┘└─────────────────────┘└┘└───────────────────────────┘┴
doc ───────┘ └┘ └┘ ┴
txt ───────┘ └┘ └┘ ┴
par ───────┘ └┘ └┘ ┴
pid ───────┘ └┘ └┘ ┴
st ─────────────────────────────────────────────────────────────────────────────────────────────────┘└─
172 ext p,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid └┘
st ──────┘└─
173 split;
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ─────────
174 simp [e.map_target] {contextual := tt}
id └┘
src └────┘ └┘ └────────────┘└┘└┘
typ └────┘└──────────┘└┘ └────────────┘└┘└┘
doc └────┘ └┘ └────────────┘ └┘
txt └────┘ └┘ └────────────┘ └┘
par └────┘ └┘ └────────────┘ └┘
pid ┴┴ ┴┴ └────────────┘ ┴┴
st ────────────────────────────────────────┘
175 end
st └─┘
176
177 /-- The total space of a basic smooth bundle is endowed with a manifold structure, where the charts
178 are in bijection with the charts of the basis. -/
179 instance to_manifold : manifold (H × F) Z.to_topological_fiber_bundle_core.total_space :=
id └──────┘ ┴ ┴ ┴ ┴└───────────────────────────────┘└──────────┘
src └──────┘ ┴ └───────────────────────────────┘└──────────┘
typ └──────┘ ┴ ┴ ┴ ┴└───────────────────────────────┘└──────────┘
doc └──────┘ └───────────────────────────────┘└──────────┘
180 { atlas := ⋃(e : local_homeomorph M H) (he : e ∈ atlas H M), {Z.chart he},
id ┴ └──────────────┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴┴└────┘ └┘
src ┴ └──────────────┘ ┴ └───┘ ┴ ┴ └────┘
typ ┴ └──────────────┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴┴└────┘ └┘
doc ┴ └──────────────┘ ┴ └────┘
181 chart_at := λp, Z.chart (chart_mem_atlas H p.1),
id ┴ ┴└────┘ └─────────────┘ ┴ ┴┴
src └────┘ └─────────────┘ ┴
typ ┴ ┴└────┘ └─────────────┘ ┴ ┴┴
doc └────┘
182 mem_chart_source := λp, by simp [mem_chart_source],
id ┴ └──────────────┘
src └────┘└──────────────┘┴
typ ┴ └────┘└──────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st └──────────────────────┘
183 chart_mem_atlas := λp, begin
id ┴
typ ┴
st └─────
184 simp only [mem_Union, mem_singleton_iff, chart_mem_atlas],
id └───────┘ └───────────────┘ └─────────────┘
src └─────────┘└───────┘└┘└───────────────┘└┘└─────────────┘┴
typ └─────────┘└───────┘└┘└───────────────┘└┘└─────────────┘┴
doc └─────────┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ ┴
st ────────────────────────────────────────────────────────────┘└─
185 exact ⟨chart_at H p.1, chart_mem_atlas H p.1, rfl⟩
id └──────┘ └─────────────┘ ┴ ┴ └─┘
src └────┘ └──────┘┴ ┴ └──┘└─────────────┘┴ ┴ └──┘└─┘└─
typ └────┘ └──────┘┴ ┴ └──┘└─────────────┘┴┴┴┴└──┘└─┘└─
doc └────┘ ┴ ┴ └──┘ ┴ ┴ └──┘ └─
txt └────┘ ┴ ┴ └──┘ ┴ ┴ └──┘ └─
par └────┘ ┴ ┴ └──┘ ┴ ┴ └──┘ └─
pid ┴ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴└
st ───────────────────────────────────────────────────────
186 end }
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
187
188 lemma mem_atlas_iff (f : local_homeomorph Z.to_topological_fiber_bundle_core.total_space (H × F)) :
id └──────────────┘ ┴└───────────────────────────────┘└──────────┘ ┴ ┴ ┴
src └──────────────┘ └───────────────────────────────┘└──────────┘ ┴
typ └──────────────┘ ┴└───────────────────────────────┘└──────────┘ ┴ ┴ ┴
doc └──────────────┘ └───────────────────────────────┘└──────────┘
189 f ∈ atlas (H × F) Z.to_topological_fiber_bundle_core.total_space ↔
id ┴ ┴ └───┘ ┴ ┴ ┴ ┴└───────────────────────────────┘└──────────┘ ┴
src ┴ └───┘ ┴ └───────────────────────────────┘└──────────┘ ┴
typ ┴ ┴ └───┘ ┴ ┴ ┴ ┴└───────────────────────────────┘└──────────┘ ┴
doc └───────────────────────────────┘└──────────┘
190 ∃(e : local_homeomorph M H) (he : e ∈ atlas H M), f = Z.chart he :=
id ┴ └──────────────┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴└────┘ └┘
src ┴ └──────────────┘ ┴ └───┘ ┴ ┴ └────┘
typ ┴ └──────────────┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴└────┘ └┘
doc └──────────────┘ └────┘
191 by simp [atlas, manifold.atlas]
src └────┘ └┘ └─
typ └────┘ └┘ └─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st └─────────────────────────────
192
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
193 @[simp] lemma mem_chart_source_iff (p q : Z.to_topological_fiber_bundle_core.total_space) :
id ┴└───────────────────────────────┘└──────────┘
src └───────────────────────────────┘└──────────┘
typ ┴└───────────────────────────────┘└──────────┘
doc └──┘ └───────────────────────────────┘└──────────┘
194 p ∈ (chart_at (H × F) q).source ↔ p.1 ∈ (chart_at H q.1).source :=
id ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴┴ ┴ └──────┘ ┴ ┴┴ └────┘
src ┴ └──────┘ ┴ └────┘ ┴ ┴ ┴ └──────┘ ┴ └────┘
typ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴┴ ┴ └──────┘ ┴ ┴┴ └────┘
195 by simp [chart_at, manifold.chart_at]
src └────┘ └┘ └─
typ └────┘ └┘ └─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st └───────────────────────────────────
196
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
197 @[simp] lemma mem_chart_target_iff (p : H × F) (q : Z.to_topological_fiber_bundle_core.total_space) :
id ┴ ┴ ┴ ┴└───────────────────────────────┘└──────────┘
src ┴ └───────────────────────────────┘└──────────┘
typ ┴ ┴ ┴ ┴└───────────────────────────────┘└──────────┘
doc └──┘ └───────────────────────────────┘└──────────┘
198 p ∈ (chart_at (H × F) q).target ↔ p.1 ∈ (chart_at H q.1).target :=
id ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴┴ ┴ └──────┘ ┴ ┴┴ └────┘
src ┴ └──────┘ ┴ └────┘ ┴ ┴ ┴ └──────┘ ┴ └────┘
typ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴┴ ┴ └──────┘ ┴ ┴┴ └────┘
199 by simp [chart_at, manifold.chart_at]
src └────┘ └┘ └─
typ └────┘ └┘ └─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st └───────────────────────────────────
200
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
201 @[simp] lemma chart_at_to_fun_fst (p q : Z.to_topological_fiber_bundle_core.total_space) :
id ┴└───────────────────────────────┘└──────────┘
src └───────────────────────────────┘└──────────┘
typ ┴└───────────────────────────────┘└──────────┘
doc └──┘ └───────────────────────────────┘└──────────┘
202 ((chart_at (H × F) q).to_fun p).1 = (chart_at H q.1).to_fun p.1 := rfl
id └──────┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └──────┘ ┴ ┴┴ └────┘ ┴┴ └─┘
src └──────┘ ┴ └────┘ ┴ ┴ └──────┘ ┴ └────┘ ┴ └─┘
typ └──────┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └──────┘ ┴ ┴┴ └────┘ ┴┴ └─┘
203
204 @[simp] lemma chart_at_inv_fun_fst (p : H × F) (q : Z.to_topological_fiber_bundle_core.total_space) :
id ┴ ┴ ┴ ┴└───────────────────────────────┘└──────────┘
src ┴ └───────────────────────────────┘└──────────┘
typ ┴ ┴ ┴ ┴└───────────────────────────────┘└──────────┘
doc └──┘ └───────────────────────────────┘└──────────┘
205 ((chart_at (H × F) q).inv_fun p).1 = (chart_at H q.1).inv_fun p.1 := rfl
id └──────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ └──────┘ ┴ ┴┴ └─────┘ ┴┴ └─┘
src └──────┘ ┴ └─────┘ ┴ ┴ └──────┘ ┴ └─────┘ ┴ └─┘
typ └──────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ └──────┘ ┴ ┴┴ └─────┘ ┴┴ └─┘
206
207 /-- Smooth manifold structure on the total space of a basic smooth bundle -/
208 instance to_smooth_manifold :
209 smooth_manifold_with_corners (I.prod (model_with_corners_self 𝕜 F))
id └──────────────────────────┘ ┴└───┘ └─────────────────────┘ ┴ ┴
src └──────────────────────────┘ └───┘ └─────────────────────┘
typ └──────────────────────────┘ ┴└───┘ └─────────────────────┘ ┴ ┴
doc └──────────────────────────┘ └───┘ └─────────────────────┘
210 Z.to_topological_fiber_bundle_core.total_space :=
id ┴└───────────────────────────────┘└──────────┘
src └───────────────────────────────┘└──────────┘
typ ┴└───────────────────────────────┘└──────────┘
doc └───────────────────────────────┘└──────────┘
211 begin
st └─────
212 /- We have to check that the charts belong to the smooth groupoid, i.e., they are smooth on their
st ────────────────────────────────────────────────────────────────────────────────────────────────────
213 source, and their inverses are smooth on the target. Since both objects are of the same type, it
st ───────────────────────────────────────────────────────────────────────────────────────────────────
214 suffices to prove the first statement in A below, and then glue back the pieces at the end. -/
st ─────────────────────────────────────────────────────────────────────────────────────────────────
215 let J := model_with_corners.to_local_equiv (I.prod (model_with_corners_self 𝕜 F)),
id └───────────────────────────────┘ └────┘ └─────────────────────┘ ┴ ┴
src └───────┘└───────────────────────────────┘┴ └────┘┴ └─────────────────────┘┴ ┴ └┘
typ └───────┘└───────────────────────────────┘┴ └────┘┴ └─────────────────────┘┴┴┴┴└┘
doc └───────┘ ┴ └────┘┴ └─────────────────────┘┴ ┴ └┘
txt └───────┘ ┴ ┴ ┴ ┴ └┘
par └───────┘ ┴ ┴ ┴ ┴ └┘
pid └───┘┴└─┘ ┴ ┴ ┴ ┴ └┘
st ──────────────────────────────────────────────────────────────────────────────────┘└─
216 have A : ∀ (e e' : local_homeomorph M H) (he : e ∈ atlas H M) (he' : e' ∈ atlas H M),
id └──────────────┘ ┴ └───┘ ┴ ┴
src └───────┘ └───────┘└──────────────┘┴ ┴ └──────┘ ┴┴┴ ┴ ┴ └───────┘ ┴ ┴└───┘┴ ┴ ┴ └
typ └───────┘ └───────┘└──────────────┘┴ ┴ └──────┘ ┴┴┴ ┴ ┴ └───────┘ ┴ ┴└───┘┴┴┴┴┴ └
doc └───────┘ └───────┘└──────────────┘┴ ┴ └──────┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ └
txt └───────┘ └───────┘ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ └
par └───────┘ └───────┘ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ └
pid └────┘└─┘ └───────┘ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ └
st ────────────────────────────────────────────────────────────────────────────────────────
217 times_cont_diff_on 𝕜 ⊤
id └────────────────┘ ┴ ┴
src ───┘└────────────────┘┴ ┴┴└
typ ───┘└────────────────┘┴┴┴┴└
doc ───┘└────────────────┘┴ ┴ └
txt ───┘ ┴ ┴ └
par ───┘ ┴ ┴ └
pid ───┘ ┴ ┴ └
st ───────────────────────────
218 (J.to_fun ∘ ((Z.chart he).symm.trans (Z.chart he')).to_fun ∘ J.inv_fun)
id ┴
src ───┘ ┴┴┴ ┴ └───────────┘ ┴ └────────┘ ┴ └─
typ ───┘ ┴┴┴ ┴ └───────────┘ ┴ └────────┘ ┴ └─
doc ───┘ ┴ ┴ ┴ └───────────┘ ┴ └────────┘ ┴ └─
txt ───┘ ┴ ┴ ┴ └───────────┘ ┴ └────────┘ ┴ └─
par ───┘ ┴ ┴ ┴ └───────────┘ ┴ └────────┘ ┴ └─
pid ───┘ ┴ ┴ ┴ └───────────┘ ┴ └────────┘ ┴ └─
st ────────────────────────────────────────────────────────────────────────────
219 (J.inv_fun ⁻¹' ((Z.chart he).symm.trans (Z.chart he')).source ∩ range J.to_fun),
id └───────┘ └─┘ └─────┘ ┴ └───┘ └──────┘
src ───┘ └───────┘┴└─┘┴ ┴ └───────────┘ └─────┘┴ └────────┘┴┴└───┘┴└──────┘┴
typ ───┘ └───────┘┴└─┘┴ ┴ └───────────┘ └─────┘┴ └────────┘┴┴└───┘┴└──────┘┴
doc ───┘ ┴└─┘┴ ┴ └───────────┘ └─────┘┴ └────────┘ ┴└───┘┴ ┴
txt ───┘ ┴ ┴ ┴ └───────────┘ ┴ └────────┘ ┴ ┴ ┴
par ───┘ ┴ ┴ ┴ └───────────┘ ┴ └────────┘ ┴ ┴ ┴
pid ───┘ ┴ ┴ ┴ └───────────┘ ┴ └────────┘ ┴ ┴ ┴
st ──────────────────────────────────────────────────────────────────────────────────┘└─
220 { assume e e' he he',
src └────────────────┘
typ └────────────────┘
doc └────────────────┘
txt └────────────────┘
par └────────────────┘
pid └────────────────┘
st ───┘└────────────────┘└─
221 have U : unique_diff_on 𝕜
id └────────────┘ ┴
src └───────┘└────────────┘┴ └
typ └───────┘└────────────┘┴┴└
doc └───────┘└────────────┘┴ └
txt └───────┘ ┴ └
par └───────┘ ┴ └
pid └────┘└─┘ ┴ └
st ──────────────────────────────
222 ((I.inv_fun ⁻¹' (e.symm.trans e').source ∩ range I.to_fun).prod (univ : set F)),
id └───────┘ └──────────┘ └┘ └───┘ └──────┘ └──┘ └─┘ ┴
src ────────────┘ └───────┘┴ ┴ └──────────┘┴ └───────┘ ┴└───┘┴└──────┘└─────┘ └──┘└─┘└─┘┴ └┘
typ ────────────┘ └───────┘┴ ┴ └──────────┘┴└┘└───────┘ ┴└───┘┴└──────┘└─────┘ └──┘└─┘└─┘┴┴└┘
doc ────────────┘ ┴ ┴ └──────────┘┴ └───────┘ ┴└───┘┴ └─────┘ └─┘ ┴ └┘
txt ────────────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ └─────┘ └─┘ ┴ └┘
par ────────────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ └─────┘ └─┘ ┴ └┘
pid ────────────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ └─────┘ └─┘ ┴ └┘
st ───────────────────────────────────────────────────────────────────────────────────────────┘└─
223 { apply unique_diff_on.prod _ unique_diff_on_univ,
id └─────────────────┘ └─────────────────┘
src └────┘└─────────────────┘└─┘└─────────────────┘
typ └────┘└─────────────────┘└─┘└─────────────────┘
doc └────┘└─────────────────┘└─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ └─┘
st ─────┘└─────────────────────────────────────────────┘└─
224 rw inter_comm,
id └────────┘
src └─┘└────────┘
typ └─┘└────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ──────────────────┘└─
225 exact I.unique_diff.inter (I.continuous_inv_fun _ (local_homeomorph.open_source _)) },
id └─────────────────┘ └──────────────────┘ └──────────────────────────┘
src └────┘└─────────────────┘┴ └──────────────────┘└─┘ └──────────────────────────┘└───┘
typ └────┘└─────────────────┘┴ └──────────────────┘└─┘ └──────────────────────────┘└───┘
doc └────┘ ┴ └─┘ └───┘
txt └────┘ ┴ └─┘ └───┘
par └────┘ ┴ └─┘ └───┘
pid ┴ ┴ └─┘ └──┘┴
st ─────────────────────────────────────────────────────────────────────────────────────────┘└┘└
226 have : J.inv_fun ⁻¹' ((chart Z he).symm.trans (chart Z he')).source ∩ range J.to_fun =
id └───────┘ └┘ └───┘ ┴ └─┘ └──────┘ ┴
src └─────┘└───────┘┴ ┴ ┴ ┴ └───────────┘ └───┘┴ ┴ └────────┘ ┴ ┴└──────┘┴┴└
typ └─────┘└───────┘┴ ┴ ┴ ┴└┘└───────────┘ └───┘┴┴┴└─┘└────────┘ ┴ ┴└──────┘┴┴└
doc └─────┘ ┴ ┴ ┴ ┴ └───────────┘ └───┘┴ ┴ └────────┘ ┴ ┴ ┴ └
txt └─────┘ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴ └────────┘ ┴ ┴ ┴ └
par └─────┘ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴ └────────┘ ┴ ┴ ┴ └
pid └───┘└┘ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴ └────────┘ ┴ ┴ ┴ └
st ───────────────────────────────────────────────────────────────────────────────────────────
227 (I.inv_fun ⁻¹' (e.symm.trans e').source ∩ range I.to_fun).prod univ,
id └───────┘ └──────────┘ └┘ └───┘ └──────┘ └──┘
src ─────┘ └───────┘┴ ┴ └──────────┘┴ └───────┘ ┴└───┘┴└──────┘└─────┘└──┘
typ ─────┘ └───────┘┴ ┴ └──────────┘┴└┘└───────┘ ┴└───┘┴└──────┘└─────┘└──┘
doc ─────┘ ┴ ┴ └──────────┘┴ └───────┘ ┴└───┘┴ └─────┘
txt ─────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ └─────┘
par ─────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ └─────┘
pid ─────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ └─────┘
st ────────────────────────────────────────────────────────────────────────┘└─
228 { have : range (λ (p : H × F), (I.to_fun (p.fst), id p.snd)) =
id ┴ ┴ ┴ └──┘ └──┘
src └─────┘ ┴ └────┘ ┴┴┴ └─┘┴ ┴ └──┘└─┘ ┴ └──┘└─┘ └
typ └─────┘ ┴ └────┘┴┴┴┴ └─┘┴ ┴ └──┘└─┘ ┴ └──┘└─┘ └
doc └─────┘ ┴ └────┘ ┴ ┴ └─┘ ┴ └─┘ ┴ └─┘ └
txt └─────┘ ┴ └────┘ ┴ ┴ └─┘ ┴ └─┘ ┴ └─┘ └
par └─────┘ ┴ └────┘ ┴ ┴ └─┘ ┴ └─┘ ┴ └─┘ └
pid └───┘└┘ ┴ └────┘ ┴ ┴ └─┘ ┴ └─┘ ┴ └─┘ └
st ─────┘└────────────────────────────────────────────────────────────
229 (range I.to_fun).prod (range (id : F → F)) := prod_range_range_eq.symm,
id └──────┘ └───┘ └┘ ┴ └──────────────────────┘
src ────────────┘ ┴└──────┘└─────┘ └───┘┴ └┘└─┘ ┴ ┴ └────┘└──────────────────────┘
typ ────────────┘ ┴└──────┘└─────┘ └───┘┴ └┘└─┘ ┴ ┴┴└────┘└──────────────────────┘
doc ────────────┘ ┴ └─────┘ └───┘┴ └─┘ ┴ ┴ └────┘
txt ────────────┘ ┴ └─────┘ ┴ └─┘ ┴ ┴ └────┘
par ────────────┘ ┴ └─────┘ ┴ └─┘ ┴ ┴ └────┘
pid ────────────┘ ┴ └─────┘ ┴ └─┘ ┴ ┴ └┘└──┘
st ──────────────────────────────────────────────────────────────────────────────────┘└─
230 simp at this,
src └──────────┘
typ └──────────┘
doc └──────────┘
txt └──────────┘
par └──────────┘
pid ┴└─────┘
st ─────────────────┘└─
231 ext p,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid └┘
st ──────────┘└─
232 simp [-mem_range, J, local_equiv.trans_source, chart, model_with_corners.prod,
id ┴ └──────────────────────┘ └───┘ └─────────────────────┘
src └────────────────┘ └┘└──────────────────────┘└┘└───┘└┘└─────────────────────┘└─
typ └────────────────┘┴└┘└──────────────────────┘└┘└───┘└┘└─────────────────────┘└─
doc └────────────────┘ └┘ └┘└───┘└┘└─────────────────────┘└─
txt └────────────────┘ └┘ └┘ └┘ └─
par └────────────────┘ └┘ └┘ └┘ └─
pid ┴└───────────┘ └┘ └┘ └┘ └─
st ─────────────────────────────────────────────────────────────────────────────────────
233 local_equiv.trans_target, this],
id └──────────────────────┘ └──┘
src ───────────┘└──────────────────────┘└┘ ┴
typ ───────────┘└──────────────────────┘└┘└──┘┴
doc ───────────┘ └┘ ┴
txt ───────────┘ └┘ ┴
par ───────────┘ └┘ ┴
pid ───────────┘ └┘ ┴
st ──────────────────────────────────────────┘└─
234 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────────┘└─
235 { tauto },
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────┘└────┘└┘└
236 { exact λ⟨⟨hx1, hx2⟩, hx3⟩, ⟨⟨⟨hx1, e.map_target hx1⟩, hx2⟩, hx3⟩ } },
id └─┘ └─┘ └─┘ └──────────┘
src └────┘ ┴ └┘ └─┘ └─┘ └┘└──────────┘┴ └─┘ └─┘ └┘
typ └────┘ ┴ └─┘└┘└─┘└─┘└─┘└─┘ └┘└──────────┘┴ └─┘ └─┘ └┘
doc └────┘ ┴ └┘ └─┘ └─┘ └┘ ┴ └─┘ └─┘ └┘
txt └────┘ ┴ └┘ └─┘ └─┘ └┘ ┴ └─┘ └─┘ └┘
par └────┘ ┴ └┘ └─┘ └─┘ └┘ ┴ └─┘ └─┘ └┘
pid ┴ ┴ └┘ └─┘ └─┘ └┘ ┴ └─┘ └─┘ ┴┴
st ───────────────────────────────────────────────────────────────────────┘└──┘└
237 rw this,
id └──┘
src └─┘
typ └─┘└──┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ──────────┘└─
238 -- check separately that the two components of the coordinate change are smooth
st ────────────────────────────────────────────────────────────────────────────────────
239 apply times_cont_diff_on.prod _ _ U,
id └─────────────────────┘ ┴
src └────┘└─────────────────────┘└───┘
typ └────┘└─────────────────────┘└───┘┴
doc └────┘└─────────────────────┘└───┘
txt └────┘ └───┘
par └────┘ └───┘
pid ┴ └───┘
st ──────────────────────────────────────┘└─
240 show times_cont_diff_on 𝕜 ⊤ (λ (p : E × F), (I.to_fun ∘ e'.to_fun ∘ e.inv_fun ∘ I.inv_fun) p.1)
id └────────────────┘ ┴ ┴ ┴ └───────┘ └───────┘
src └───┘└────────────────┘┴ ┴ ┴ └────┘ ┴ ┴ └─┘ ┴ ┴└───────┘┴ ┴└───────┘┴ ┴ └┘ └───
typ └───┘└────────────────┘┴┴┴ ┴ └────┘┴┴┴┴ └─┘ ┴ ┴└───────┘┴ ┴└───────┘┴ ┴ └┘ └───
doc └───┘└────────────────┘┴ ┴ ┴ └────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └───
txt └───┘ ┴ ┴ ┴ └────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └───
par └───┘ ┴ ┴ ┴ └────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └───
pid └───┘ ┴ ┴ ┴ └────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └───
st ────────────────────────────────────────────────────────────────────────────────────────────────────
241 ((I.inv_fun ⁻¹' (e.symm.trans e').source ∩ range I.to_fun).prod (univ : set F)),
id └───────┘ └──────────┘ └┘ └───┘ └──────┘ └──┘ └─┘ ┴
src ────────┘ └───────┘┴ ┴ └──────────┘┴ └───────┘ ┴└───┘┴└──────┘└─────┘ └──┘└─┘└─┘┴ └┘
typ ────────┘ └───────┘┴ ┴ └──────────┘┴└┘└───────┘ ┴└───┘┴└──────┘└─────┘ └──┘└─┘└─┘┴┴└┘
doc ────────┘ ┴ ┴ └──────────┘┴ └───────┘ ┴└───┘┴ └─────┘ └─┘ ┴ └┘
txt ────────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ └─────┘ └─┘ ┴ └┘
par ────────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ └─────┘ └─┘ ┴ └┘
pid ────────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ └─────┘ └─┘ ┴ └┘
st ───────────────────────────────────────────────────────────────────────────────────────┘└─
242 { -- the coordinate change on the base is just a coordinate change for `M`, smooth since
st ─────┘└──────────────────────────────────────────────────────────────────────────────────────
243 -- `M` is smooth
st ───────────────────────
244 have A : times_cont_diff_on 𝕜 ⊤
id └────────────────┘ ┴
src └───────┘└────────────────┘┴ ┴ └
typ └───────┘└────────────────┘┴┴┴ └
doc └───────┘└────────────────┘┴ ┴ └
txt └───────┘ ┴ ┴ └
par └───────┘ ┴ ┴ └
pid └────┘└─┘ ┴ ┴ └
st ──────────────────────────────────────
245 (I.to_fun ∘ (e.symm.trans e').to_fun ∘ I.inv_fun)
src ───────┘ ┴ ┴ ┴ └───────┘ ┴ └─
typ ───────┘ ┴ ┴ ┴ └───────┘ ┴ └─
doc ───────┘ ┴ ┴ ┴ └───────┘ ┴ └─
txt ───────┘ ┴ ┴ ┴ └───────┘ ┴ └─
par ───────┘ ┴ ┴ ┴ └───────┘ ┴ └─
pid ───────┘ ┴ ┴ ┴ └───────┘ ┴ └─
st ──────────────────────────────────────────────────────────
246 (I.inv_fun ⁻¹' (e.symm.trans e').source ∩ range I.to_fun) :=
id └───────┘ └──────────┘ └┘ └───┘ └──────┘
src ───────┘ └───────┘┴ ┴ └──────────┘┴ └───────┘ ┴└───┘┴└──────┘└────
typ ───────┘ └───────┘┴ ┴ └──────────┘┴└┘└───────┘ ┴└───┘┴└──────┘└────
doc ───────┘ ┴ ┴ └──────────┘┴ └───────┘ ┴└───┘┴ └────
txt ───────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ └────
par ───────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ └────
pid ───────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴└───
st ─────────────────────────────────────────────────────────────────────
247 (has_groupoid.compatible (times_cont_diff_groupoid ⊤ I) he he').1,
id └─────────────────────┘ └──────────────────────┘ ┴ └┘ └─┘
src ───────┘ └─────────────────────┘┴ └──────────────────────┘┴ ┴ └┘ ┴ └─┘
typ ───────┘ └─────────────────────┘┴ └──────────────────────┘┴ ┴┴└┘└┘┴└─┘└─┘
doc ───────┘ ┴ └──────────────────────┘┴ ┴ └┘ ┴ └─┘
txt ───────┘ ┴ ┴ ┴ └┘ ┴ └─┘
par ───────┘ ┴ ┴ ┴ └┘ ┴ └─┘
pid ───────┘ ┴ ┴ ┴ └┘ ┴ ┴└┘
st ────────────────────────────────────────────────────────────────────────┘└─
248 have B : times_cont_diff_on 𝕜 ⊤ (λp : E × F, p.1)
id └────────────────┘ ┴ ┴ ┴
src └───────┘└────────────────┘┴ ┴ ┴ └──┘ ┴ ┴ └┘ └───
typ └───────┘└────────────────┘┴┴┴ ┴ └──┘┴┴ ┴┴└┘ └───
doc └───────┘└────────────────┘┴ ┴ ┴ └──┘ ┴ ┴ └┘ └───
txt └───────┘ ┴ ┴ ┴ └──┘ ┴ ┴ └┘ └───
par └───────┘ ┴ ┴ ┴ └──┘ ┴ ┴ └┘ └───
pid └────┘└─┘ ┴ ┴ ┴ └──┘ ┴ ┴ └┘ └───
st ────────────────────────────────────────────────────────
249 ((I.inv_fun ⁻¹' (e.symm.trans e').source ∩ range I.to_fun).prod univ) :=
id └───────┘ └──────────┘ └┘ └───┘ └──────┘ └──┘
src ───────┘ └───────┘┴ ┴ └──────────┘┴ └───────┘ ┴└───┘┴└──────┘└─────┘└──┘└────
typ ───────┘ └───────┘┴ ┴ └──────────┘┴└┘└───────┘ ┴└───┘┴└──────┘└─────┘└──┘└────
doc ───────┘ ┴ ┴ └──────────┘┴ └───────┘ ┴└───┘┴ └─────┘ └────
txt ───────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ └─────┘ └────
par ───────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ └─────┘ └────
pid ───────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ └─────┘ ┴└───
st ─────────────────────────────────────────────────────────────────────────────────
250 times_cont_diff_fst.times_cont_diff_on U,
id └────────────────────────────────────┘ ┴
src ─────┘└────────────────────────────────────┘┴
typ ─────┘└────────────────────────────────────┘┴┴
doc ─────┘└────────────────────────────────────┘┴
txt ─────┘ ┴
par ─────┘ ┴
pid ─────┘ ┴
st ─────────────────────────────────────────────┘└─
251 exact times_cont_diff_on.comp A B U (prod_subset_preimage_fst _ _) },
id └─────────────────────┘ ┴ ┴ ┴ └──────────────────────┘
src └────┘└─────────────────────┘┴ ┴ ┴ ┴ └──────────────────────┘└────┘
typ └────┘└─────────────────────┘┴┴┴┴┴┴┴ └──────────────────────┘└────┘
doc └────┘└─────────────────────┘┴ ┴ ┴ ┴ └────┘
txt └────┘ ┴ ┴ ┴ ┴ └────┘
par └────┘ ┴ ┴ ┴ ┴ └────┘
pid ┴ ┴ ┴ ┴ ┴ └───┘┴
st ────────────────────────────────────────────────────────────────────────┘└┘└
252 show times_cont_diff_on 𝕜 ⊤ (λ (p : E × F),
id └────────────────┘ ┴ ┴
src └───┘└────────────────┘┴ ┴ ┴ └────┘ ┴ ┴ └──
typ └───┘└────────────────┘┴┴┴ ┴ └────┘┴┴ ┴ └──
doc └───┘└────────────────┘┴ ┴ ┴ └────┘ ┴ ┴ └──
txt └───┘ ┴ ┴ ┴ └────┘ ┴ ┴ └──
par └───┘ ┴ ┴ ┴ └────┘ ┴ ┴ └──
pid └───┘ ┴ ┴ ┴ └────┘ ┴ ┴ └──
st ────────────────────────────────────────────────
253 Z.coord_change ⟨chart_at H (e.inv_fun (I.inv_fun p.1)), _⟩ ⟨e', he'⟩
id └─┘
src ─────┘ ┴ ┴ ┴ ┴ ┴ └───────┘ └┘ └─
typ ─────┘ ┴ ┴ ┴ ┴ ┴ └───────┘ └┘└─┘└─
doc ─────┘ ┴ ┴ ┴ ┴ ┴ └───────┘ └┘ └─
txt ─────┘ ┴ ┴ ┴ ┴ ┴ └───────┘ └┘ └─
par ─────┘ ┴ ┴ ┴ ┴ ┴ └───────┘ └┘ └─
pid ─────┘ ┴ ┴ ┴ ┴ ┴ └───────┘ └┘ └─
st ───────────────────────────────────────────────────────────────────────────
254 ((chart_at H (e.inv_fun (I.inv_fun p.1))).to_fun (e.inv_fun (I.inv_fun p.1)))
src ────────┘ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴ └─────
typ ────────┘ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴ └─────
doc ────────┘ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴ └─────
txt ────────┘ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴ └─────
par ────────┘ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴ └─────
pid ────────┘ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴ └─────
st ───────────────────────────────────────────────────────────────────────────────────────
255 (Z.coord_change ⟨e, he⟩ ⟨chart_at H (e.inv_fun (I.inv_fun p.1)), _⟩
id └────────────┘ └┘ └──────┘ ┴
src ─────┘ └────────────┘┴ └┘ └┘ └──────┘┴ ┴ ┴ ┴ └────────
typ ─────┘ └────────────┘┴ └┘└┘└┘ └──────┘┴┴┴ ┴ ┴ └────────
doc ─────┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ └────────
txt ─────┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ └────────
par ─────┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ └────────
pid ─────┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ └────────
st ──────────────────────────────────────────────────────────────────────────
256 (e.to_fun (e.inv_fun (I.inv_fun p.1))) p.2))
id └──────┘ └───────┘
src ───────┘ └──────┘┴ └───────┘┴ ┴ └────┘ └────
typ ───────┘ └──────┘┴ └───────┘┴ ┴ └────┘ └────
doc ───────┘ ┴ ┴ ┴ └────┘ └────
txt ───────┘ ┴ ┴ ┴ └────┘ └────
par ───────┘ ┴ ┴ ┴ └────┘ └────
pid ───────┘ ┴ ┴ ┴ └────┘ └────
st ─────────────────────────────────────────────────────
257 ((I.inv_fun ⁻¹' (e.symm.trans e').source ∩ range I.to_fun).prod (univ : set F)),
id └───────┘ └──────────┘ └┘ └───┘ └──────┘ └──┘ └─┘ ┴
src ─────┘ └───────┘┴ ┴ └──────────┘┴ └───────┘ ┴└───┘┴└──────┘└─────┘ └──┘└─┘└─┘┴ └┘
typ ─────┘ └───────┘┴ ┴ └──────────┘┴└┘└───────┘ ┴└───┘┴└──────┘└─────┘ └──┘└─┘└─┘┴┴└┘
doc ─────┘ ┴ ┴ └──────────┘┴ └───────┘ ┴└───┘┴ └─────┘ └─┘ ┴ └┘
txt ─────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ └─────┘ └─┘ ┴ └┘
par ─────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ └─────┘ └─┘ ┴ └┘
pid ─────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ └─────┘ └─┘ ┴ └┘
st ────────────────────────────────────────────────────────────────────────────────────┘└─
258 { /- The coordinate change in the fiber is more complicated as its definition involves the
st ───────────────────────────────────────────────────────────────────────────────────────────────
259 reference chart chosen at each point. However, it appears with its inverse, so using the
st ───────────────────────────────────────────────────────────────────────────────────────────────
260 cocycle property one can get rid of it, and then conclude using the smoothness of the
st ────────────────────────────────────────────────────────────────────────────────────────────
261 cocycle as given in the definition of basic smooth bundles. -/
st ─────────────────────────────────────────────────────────────────────
262 have := Z.coord_change_smooth ⟨e, he⟩ ⟨e', he'⟩,
id └───────────────────┘ ┴ └┘ └┘ └─┘
src └──────┘└───────────────────┘┴ └┘ └┘ └┘ ┴
typ └──────┘└───────────────────┘┴ ┴└┘└┘└┘ └┘└┘└─┘┴
doc └──────┘ ┴ └┘ └┘ └┘ ┴
txt └──────┘ ┴ └┘ └┘ └┘ ┴
par └──────┘ ┴ └┘ └┘ └┘ ┴
pid └───┘└─┘ ┴ └┘ └┘ └┘ ┴
st ────────────────────────────────────────────────────┘└─
263 rw model_with_corners.image at this,
id └──────────────────────┘
src └─┘└──────────────────────┘└──────┘
typ └─┘└──────────────────────┘└──────┘
doc └─┘ └──────┘
txt └─┘ └──────┘
par └─┘ └──────┘
pid ┴ └──────┘
st ────────────────────────────────────────┘└─
264 apply times_cont_diff_on.congr this U,
id └──────────────────────┘ └──┘ ┴
src └────┘└──────────────────────┘┴ ┴
typ └────┘└──────────────────────┘┴└──┘┴┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ──────────────────────────────────────────┘└─
265 rintros ⟨x, v⟩ hx,
src └───────────────┘
typ └───────────────┘
doc └───────────────┘
txt └───────────────┘
par └───────────────┘
pid └────────┘
st ──────────────────────┘└─
266 simp [local_equiv.trans_source] at hx,
id └──────────────────────┘
src └────┘└──────────────────────┘└─────┘
typ └────┘└──────────────────────┘└─────┘
doc └────┘ └─────┘
txt └────┘ └─────┘
par └────┘ └─────┘
pid ┴┴ ┴┴└───┘
st ──────────────────────────────────────────┘└─
267 let f := chart_at H (e.inv_fun (I.inv_fun x)),
id └──────┘ ┴ └───────┘ └───────┘ ┴
src └───────┘└──────┘┴ ┴ └───────┘┴ └───────┘┴ └┘
typ └───────┘└──────┘┴┴┴ └───────┘┴ └───────┘┴┴└┘
doc └───────┘ ┴ ┴ ┴ ┴ └┘
txt └───────┘ ┴ ┴ ┴ ┴ └┘
par └───────┘ ┴ ┴ ┴ ┴ └┘
pid └───┘┴└─┘ ┴ ┴ ┴ ┴ └┘
st ──────────────────────────────────────────────────┘└─
268 have A : I.inv_fun x ∈ ((e.symm.trans f).trans (f.symm.trans e')).source,
id └───────┘ ┴ └──────────┘ └──────────┘ └┘
src └───────┘└───────┘┴ ┴ ┴ └──────────┘┴ └──────┘ └──────────┘┴ └───────┘
typ └───────┘└───────┘┴┴┴ ┴ └──────────┘┴ └──────┘ └──────────┘┴└┘└───────┘
doc └───────┘ ┴ ┴ ┴ └──────────┘┴ └──────┘ └──────────┘┴ └───────┘
txt └───────┘ ┴ ┴ ┴ ┴ └──────┘ ┴ └───────┘
par └───────┘ ┴ ┴ ┴ ┴ └──────┘ ┴ └───────┘
pid └────┘└─┘ ┴ ┴ ┴ ┴ └──────┘ ┴ └──────┘┴
st ─────────────────────────────────────────────────────────────────────────────┘
269 by simp [local_equiv.trans_source, hx.1.1, hx.1.2, mem_chart_source, f.map_source],
id └──────────────────────┘ └┘ └┘ └──────────────┘
src └────┘└──────────────────────┘└┘ └────┘ └────┘└──────────────┘└┘ ┴
typ └────┘└──────────────────────┘└┘└┘└────┘└┘└────┘└──────────────┘└┘└──────────┘┴
doc └────┘ └┘ └────┘ └────┘ └┘ ┴
txt └────┘ └┘ └────┘ └────┘ └┘ ┴
par └────┘ └┘ └────┘ └────┘ └┘ ┴
pid ┴┴ └┘ └────┘ └────┘ └┘ ┴
st └─
270 rw e.right_inv hx.1.1,
id └─────────┘ └┘
src └─┘└─────────┘┴ └──┘
typ └─┘└─────────┘┴└┘└──┘
doc └─┘ ┴ └──┘
txt └─┘ ┴ └──┘
par └─┘ ┴ └──┘
pid ┴ ┴ └┘└┘
st ──────────────────────────┘└─
271 have := Z.coord_change_comp ⟨e, he⟩ ⟨f, chart_mem_atlas _ _⟩ ⟨e', he'⟩ (I.inv_fun x) A v,
id └─────────────────┘ ┴ └┘ ┴ └─────────────┘ └┘ └─┘ └───────┘ ┴ ┴ ┴
src └──────┘└─────────────────┘┴ └┘ └┘ └┘└─────────────┘└────┘ └┘ └┘ └───────┘┴ └┘ ┴
typ └──────┘└─────────────────┘┴ ┴└┘└┘└┘ ┴└┘└─────────────┘└────┘ └┘└┘└─┘└┘ └───────┘┴┴└┘┴┴┴
doc └──────┘ ┴ └┘ └┘ └┘ └────┘ └┘ └┘ ┴ └┘ ┴
txt └──────┘ ┴ └┘ └┘ └┘ └────┘ └┘ └┘ ┴ └┘ ┴
par └──────┘ ┴ └┘ └┘ └┘ └────┘ └┘ └┘ ┴ └┘ ┴
pid └───┘└─┘ ┴ └┘ └┘ └┘ └────┘ └┘ └┘ ┴ └┘ ┴
st ─────────────────────────────────────────────────────────────────────────────────────────────┘└─
272 simpa using this } },
id └──┘
src └──────────┘ ┴
typ └──────────┘└──┘┴
doc └──────────┘ ┴
txt └──────────┘ ┴
par └──────────┘ ┴
pid ┴└────┘ ┴
st ──────────────────────┘└──┘└
273 haveI : has_groupoid Z.to_topological_fiber_bundle_core.total_space
id └──────────┘ └────────────────────────────────────────────┘
src └──────┘└──────────┘┴└────────────────────────────────────────────┘└
typ └──────┘└──────────┘┴└────────────────────────────────────────────┘└
doc └──────┘└──────────┘┴└────────────────────────────────────────────┘└
txt └──────┘ ┴ └
par └──────┘ ┴ └
pid ┴└┘ ┴ └
st ──────────────────────────────────────────────────────────────────────
274 (times_cont_diff_groupoid ⊤ (I.prod (model_with_corners_self 𝕜 F))) :=
id └──────────────────────┘ └────┘ └─────────────────────┘ ┴ ┴
src ────────┘ └──────────────────────┘┴ ┴ └────┘┴ └─────────────────────┘┴ ┴ └──────
typ ────────┘ └──────────────────────┘┴ ┴ └────┘┴ └─────────────────────┘┴┴┴┴└──────
doc ────────┘ └──────────────────────┘┴ ┴ └────┘┴ └─────────────────────┘┴ ┴ └──────
txt ────────┘ ┴ ┴ ┴ ┴ ┴ └──────
par ────────┘ ┴ ┴ ┴ ┴ ┴ └──────
pid ────────┘ ┴ ┴ ┴ ┴ ┴ └─┘└───
st ────────────────────────────────────────────────────────────────────────────────
275 begin
src ─┘ └
typ ─┘ └
doc ─┘ └
txt ─┘ └
par ─┘ └
pid ─┘ └
st ─┘└─────
276 split,
src ───┘└───┘└─
typ ───┘└───┘└─
doc ───┘└───┘└─
txt ───┘└───┘└─
par ───┘└───┘└─
pid ───────────
st ────────┘└─
277 assume e₀ e₀' he₀ he₀',
src ───┘└────────────────────┘└─
typ ───┘└────────────────────┘└─
doc ───┘└────────────────────┘└─
txt ───┘└────────────────────┘└─
par ───┘└────────────────────┘└─
pid ────────────────────────────
st ─────────────────────────┘└─
278 rcases (Z.mem_atlas_iff _).1 he₀ with ⟨e, he, rfl⟩,
id └─────────────┘ └─┘
src ───┘└─────┘ └─────────────┘└────┘ └────────────────┘└─
typ ───┘└─────┘ └─────────────┘└────┘└─┘└────────────────┘└─
doc ───┘└─────┘ └────┘ └────────────────┘└─
txt ───┘└─────┘ └────┘ └────────────────┘└─
par ───┘└─────┘ └────┘ └────────────────┘└─
pid ──────────┘ └────┘ └───────────────────
st ─────────────────────────────────────────────────────┘└─
279 rcases (Z.mem_atlas_iff _).1 he₀' with ⟨e', he', rfl⟩,
id └─────────────┘ └──┘
src ───┘└─────┘ └─────────────┘└────┘ └──────────────────┘└─
typ ───┘└─────┘ └─────────────┘└────┘└──┘└──────────────────┘└─
doc ───┘└─────┘ └────┘ └──────────────────┘└─
txt ───┘└─────┘ └────┘ └──────────────────┘└─
par ───┘└─────┘ └────┘ └──────────────────┘└─
pid ──────────┘ └────┘ └─────────────────────
st ────────────────────────────────────────────────────────┘└─
280 rw [times_cont_diff_groupoid, mem_groupoid_of_pregroupoid],
id └──────────────────────┘ └─────────────────────────┘
src ───┘└──┘└──────────────────────┘└┘└─────────────────────────┘┴└─
typ ───┘└──┘└──────────────────────┘└┘└─────────────────────────┘┴└─
doc ───┘└──┘└──────────────────────┘└┘ ┴└─
txt ───┘└──┘ └┘ ┴└─
par ───┘└──┘ └┘ ┴└─
pid ───────┘ └┘ └──
st ───────────────────────────────┘└───────────────────────────┘└──
281 exact ⟨A e e' he he', A e' e he' he⟩
id ┴ └┘ ┴ └─┘ └┘
src ───┘└────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─
typ ───┘└────┘ ┴ ┴ ┴ ┴ └┘┴┴└┘┴┴┴└─┘┴└┘└─
doc ───┘└────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─
txt ───┘└────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─
par ───┘└────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─
pid ─────────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─
st ─────────────────────────────────────────
282 end,
src ─┘└─┘
typ ─┘└─┘
doc ─┘└─┘
txt ─┘└─┘
par ─┘└─┘
pid ────┘
st ─┘└─┘└─
283 constructor
src └──────────┘
typ └──────────┘
doc └──────────┘
txt └──────────┘
par └──────────┘
pid ┴
st ─────────────┘
284 end
st └─┘
285
286 end basic_smooth_bundle_core
287
288 section tangent_bundle
289
290 variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
id ┴ └──────────────────────┘
src └──────────────────────┘
typ ┴ └──────────────────────┘
doc └──────────────────────┘
291 {E : Type u} [normed_group E] [normed_space 𝕜 E]
id └──────────┘ └──────────┘
src └──────────┘ └──────────┘
typ └──────────┘ └──────────┘
doc └──────────┘ └──────────┘
292 {H : Type*} [topological_space H] (I : model_with_corners 𝕜 E H)
id └───────────────┘ └────────────────┘
src └───────────────┘ └────────────────┘
typ └───────────────┘ └────────────────┘
doc └───────────────┘ └────────────────┘
293 (M : Type*) [topological_space M] [manifold H M] [smooth_manifold_with_corners I M]
id └───────────────┘ └──────┘ └──────────────────────────┘
src └───────────────┘ └──────┘ └──────────────────────────┘
typ └───────────────┘ └──────┘ └──────────────────────────┘
doc └───────────────┘ └──────┘ └──────────────────────────┘
294
295 set_option class.instance_max_depth 50
doc └──────────────────────┘
296
297 /-- Basic smooth bundle core version of the tangent bundle of a smooth manifold `M` modelled over a
298 model with corners `I` on `(E, H)`. The fibers are equal to `E`, and the coordinate change in the
299 fiber corresponds to the derivative of the coordinate change in `M`. -/
300 def tangent_bundle_core : basic_smooth_bundle_core I M E :=
id └──────────────────────┘ ┴ ┴ ┴
src └──────────────────────┘
typ └──────────────────────┘ ┴ ┴ ┴
doc └──────────────────────┘
301 { coord_change := λi j x v, (fderiv_within 𝕜 (I.to_fun ∘ j.1.to_fun ∘ i.1.inv_fun ∘ I.inv_fun)
id ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴└─────┘ ┴ ┴┴ └────┘ ┴ ┴┴ └─────┘ ┴ ┴└──────┘
src └───────────┘ └─────┘ ┴ ┴ └────┘ ┴ ┴ └─────┘ ┴ └──────┘
typ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴└─────┘ ┴ ┴┴ └────┘ ┴ ┴┴ └─────┘ ┴ ┴└──────┘
doc └───────────┘
302 (range I.to_fun) (I.to_fun x) : E → E) v,
id └───┘ ┴└─────┘ ┴└─────┘ ┴ ┴ ┴ ┴
src └───┘ └─────┘ └─────┘
typ └───┘ ┴└─────┘ ┴└─────┘ ┴ ┴ ┴ ┴
doc └───┘
303 coord_change_smooth := λi j, begin
id ┴ ┴
typ ┴ ┴
st └─────
304 /- To check that the coordinate change of the bundle is smooth, one should just use the
st ────────────────────────────────────────────────────────────────────────────────────────────
305 smoothness of the charts, and thus the smoothness of their derivatives. -/
st ───────────────────────────────────────────────────────────────────────────────
306 rw model_with_corners.image,
id └──────────────────────┘
src └─┘└──────────────────────┘
typ └─┘└──────────────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ──────────────────────────────┘└─
307 have A : times_cont_diff_on 𝕜 ⊤
id └────────────────┘ ┴
src └───────┘└────────────────┘┴ ┴ └
typ └───────┘└────────────────┘┴┴┴ └
doc └───────┘└────────────────┘┴ ┴ └
txt └───────┘ ┴ ┴ └
par └───────┘ ┴ ┴ └
pid └────┘└─┘ ┴ ┴ └
st ────────────────────────────────────
308 (I.to_fun ∘ (i.1.symm.trans j.1).to_fun ∘ I.inv_fun)
src ─────┘ ┴ ┴ └────────────┘ └─────────┘ ┴ └─
typ ─────┘ ┴ ┴ └────────────┘ └─────────┘ ┴ └─
doc ─────┘ ┴ ┴ └────────────┘ └─────────┘ ┴ └─
txt ─────┘ ┴ ┴ └────────────┘ └─────────┘ ┴ └─
par ─────┘ ┴ ┴ └────────────┘ └─────────┘ ┴ └─
pid ─────┘ ┴ ┴ └────────────┘ └─────────┘ ┴ └─
st ───────────────────────────────────────────────────────────
309 (I.inv_fun ⁻¹' (i.1.symm.trans j.1).source ∩ range I.to_fun) :=
id └───────┘ ┴ ┴ └───┘ └──────┘
src ─────┘ └───────┘┴ ┴ └────────────┘ └─────────┘ ┴└───┘┴└──────┘└────
typ ─────┘ └───────┘┴ ┴ ┴└────────────┘┴└─────────┘ ┴└───┘┴└──────┘└────
doc ─────┘ ┴ ┴ └────────────┘ └─────────┘ ┴└───┘┴ └────
txt ─────┘ ┴ ┴ └────────────┘ └─────────┘ ┴ ┴ └────
par ─────┘ ┴ ┴ └────────────┘ └─────────┘ ┴ ┴ └────
pid ─────┘ ┴ ┴ └────────────┘ └─────────┘ ┴ ┴ ┴└───
st ──────────────────────────────────────────────────────────────────────
310 (has_groupoid.compatible (times_cont_diff_groupoid ⊤ I) i.2 j.2).1,
id └─────────────────────┘ └──────────────────────┘ ┴ ┴ ┴
src ─────┘ └─────────────────────┘┴ └──────────────────────┘┴ ┴ └┘ └─┘ └───┘
typ ─────┘ └─────────────────────┘┴ └──────────────────────┘┴ ┴┴└┘┴└─┘┴└───┘
doc ─────┘ ┴ └──────────────────────┘┴ ┴ └┘ └─┘ └───┘
txt ─────┘ ┴ ┴ ┴ └┘ └─┘ └───┘
par ─────┘ ┴ ┴ ┴ └┘ └─┘ └───┘
pid ─────┘ ┴ ┴ ┴ └┘ └─┘ └─┘└┘
st ───────────────────────────────────────────────────────────────────────┘└─
311 have B : unique_diff_on 𝕜 (I.inv_fun ⁻¹' (i.1.symm.trans j.1).source ∩ range I.to_fun),
id └────────────┘ ┴ └───────┘ ┴ ┴ └───┘ └──────┘
src └───────┘└────────────┘┴ ┴ └───────┘┴ ┴ └────────────┘ └─────────┘ ┴└───┘┴└──────┘┴
typ └───────┘└────────────┘┴┴┴ └───────┘┴ ┴ ┴└────────────┘┴└─────────┘ ┴└───┘┴└──────┘┴
doc └───────┘└────────────┘┴ ┴ ┴ ┴ └────────────┘ └─────────┘ ┴└───┘┴ ┴
txt └───────┘ ┴ ┴ ┴ ┴ └────────────┘ └─────────┘ ┴ ┴ ┴
par └───────┘ ┴ ┴ ┴ ┴ └────────────┘ └─────────┘ ┴ ┴ ┴
pid └────┘└─┘ ┴ ┴ ┴ ┴ └────────────┘ └─────────┘ ┴ ┴ ┴
st ─────────────────────────────────────────────────────────────────────────────────────────┘└─
312 { rw inter_comm,
id └────────┘
src └─┘└────────┘
typ └─┘└────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ─────┘└───────────┘└─
313 apply I.unique_diff.inter (I.continuous_inv_fun _ (local_homeomorph.open_source _)) },
id └─────────────────┘ └──────────────────┘ └──────────────────────────┘
src └────┘└─────────────────┘┴ └──────────────────┘└─┘ └──────────────────────────┘└───┘
typ └────┘└─────────────────┘┴ └──────────────────┘└─┘ └──────────────────────────┘└───┘
doc └────┘ ┴ └─┘ └───┘
txt └────┘ ┴ └─┘ └───┘
par └────┘ ┴ └─┘ └───┘
pid ┴ ┴ └─┘ └──┘┴
st ─────────────────────────────────────────────────────────────────────────────────────────┘└┘└
314 have C : times_cont_diff_on 𝕜 ⊤
id └────────────────┘
src └───────┘└────────────────┘┴ ┴ └
typ └───────┘└────────────────┘┴ ┴ └
doc └───────┘└────────────────┘┴ ┴ └
txt └───────┘ ┴ ┴ └
par └───────┘ ┴ ┴ └
pid └────┘└─┘ ┴ ┴ └
st ────────────────────────────────────
315 (λ (p : E × E), (fderiv_within 𝕜 (I.to_fun ∘ j.1.to_fun ∘ i.1.inv_fun ∘ I.inv_fun)
id ┴ └───────────┘ ┴
src ─────┘ └────┘ ┴┴┴ └─┘ └───────────┘┴ ┴ ┴ ┴ └────────┘ ┴ └─────────┘ ┴ └─
typ ─────┘ └────┘ ┴┴┴ └─┘ └───────────┘┴┴┴ ┴ ┴ └────────┘ ┴ └─────────┘ ┴ └─
doc ─────┘ └────┘ ┴ ┴ └─┘ └───────────┘┴ ┴ ┴ ┴ └────────┘ ┴ └─────────┘ ┴ └─
txt ─────┘ └────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └────────┘ ┴ └─────────┘ ┴ └─
par ─────┘ └────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └────────┘ ┴ └─────────┘ ┴ └─
pid ─────┘ └────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └────────┘ ┴ └─────────┘ ┴ └─
st ─────────────────────────────────────────────────────────────────────────────────────────
316 (I.inv_fun ⁻¹' (i.1.symm.trans j.1).source ∩ range I.to_fun) p.1 : E → E) p.2)
id ┴
src ───────────┘ ┴ ┴ └────────────┘ └─────────┘ ┴ ┴ └┘ └───┘ ┴ ┴ └┘ └───
typ ───────────┘ ┴ ┴ └────────────┘ └─────────┘ ┴ ┴ └┘ └───┘ ┴ ┴┴└┘ └───
doc ───────────┘ ┴ ┴ └────────────┘ └─────────┘ ┴ ┴ └┘ └───┘ ┴ ┴ └┘ └───
txt ───────────┘ ┴ ┴ └────────────┘ └─────────┘ ┴ ┴ └┘ └───┘ ┴ ┴ └┘ └───
par ───────────┘ ┴ ┴ └────────────┘ └─────────┘ ┴ ┴ └┘ └───┘ ┴ ┴ └┘ └───
pid ───────────┘ ┴ ┴ └────────────┘ └─────────┘ ┴ ┴ └┘ └───┘ ┴ ┴ └┘ └───
st ───────────────────────────────────────────────────────────────────────────────────────────
317 ((I.inv_fun ⁻¹' (i.1.symm.trans j.1).source ∩ range I.to_fun).prod univ) :=
id └───────┘ ┴ ┴ └───┘ └──────┘ └──┘
src ─────┘ └───────┘┴ ┴ └────────────┘ └─────────┘ ┴└───┘┴└──────┘└─────┘└──┘└────
typ ─────┘ └───────┘┴ ┴ ┴└────────────┘┴└─────────┘ ┴└───┘┴└──────┘└─────┘└──┘└────
doc ─────┘ ┴ ┴ └────────────┘ └─────────┘ ┴└───┘┴ └─────┘ └────
txt ─────┘ ┴ ┴ └────────────┘ └─────────┘ ┴ ┴ └─────┘ └────
par ─────┘ ┴ ┴ └────────────┘ └─────────┘ ┴ ┴ └─────┘ └────
pid ─────┘ ┴ ┴ └────────────┘ └─────────┘ ┴ ┴ └─────┘ ┴└───
st ──────────────────────────────────────────────────────────────────────────────────
318 times_cont_diff_on_fderiv_within_apply A B lattice.le_top,
id └────────────────────────────────────┘ ┴ ┴ └────────────┘
src ─────┘└────────────────────────────────────┘┴ ┴ ┴└────────────┘
typ ─────┘└────────────────────────────────────┘┴┴┴┴┴└────────────┘
doc ─────┘└────────────────────────────────────┘┴ ┴ ┴
txt ─────┘ ┴ ┴ ┴
par ─────┘ ┴ ┴ ┴
pid ─────┘ ┴ ┴ ┴
st ──────────────────────────────────────────────────────────────┘└─
319 have D : ∀ x ∈ (I.inv_fun ⁻¹' (i.1.symm.trans j.1).source ∩ range I.to_fun),
src └───────┘ └───┘ ┴ ┴ └────────────┘ └─────────┘ ┴ ┴ ┴ └
typ └───────┘ └───┘ ┴ ┴ └────────────┘ └─────────┘ ┴ ┴ ┴ └
doc └───────┘ └───┘ ┴ ┴ └────────────┘ └─────────┘ ┴ ┴ ┴ └
txt └───────┘ └───┘ ┴ ┴ └────────────┘ └─────────┘ ┴ ┴ ┴ └
par └───────┘ └───┘ ┴ ┴ └────────────┘ └─────────┘ ┴ ┴ ┴ └
pid └────┘└─┘ └───┘ ┴ ┴ └────────────┘ └─────────┘ ┴ ┴ ┴ └
st ─────────────────────────────────────────────────────────────────────────────────
320 fderiv_within 𝕜 (I.to_fun ∘ j.1.to_fun ∘ i.1.inv_fun ∘ I.inv_fun)
src ─────┘ ┴ ┴ ┴ ┴ └────────┘ ┴ └─────────┘ ┴ └─
typ ─────┘ ┴ ┴ ┴ ┴ └────────┘ ┴ └─────────┘ ┴ └─
doc ─────┘ ┴ ┴ ┴ ┴ └────────┘ ┴ └─────────┘ ┴ └─
txt ─────┘ ┴ ┴ ┴ ┴ └────────┘ ┴ └─────────┘ ┴ └─
par ─────┘ ┴ ┴ ┴ ┴ └────────┘ ┴ └─────────┘ ┴ └─
pid ─────┘ ┴ ┴ ┴ ┴ └────────┘ ┴ └─────────┘ ┴ └─
st ────────────────────────────────────────────────────────────────────────
321 (range I.to_fun) x =
src ───────────┘ ┴ └┘ ┴ └
typ ───────────┘ ┴ └┘ ┴ └
doc ───────────┘ ┴ └┘ ┴ └
txt ───────────┘ ┴ └┘ ┴ └
par ───────────┘ ┴ └┘ ┴ └
pid ───────────┘ ┴ └┘ ┴ └
st ─────────────────────────────────
322 fderiv_within 𝕜 (I.to_fun ∘ j.1.to_fun ∘ i.1.inv_fun ∘ I.inv_fun)
id └───────────┘ ┴
src ─────┘└───────────┘┴ ┴ ┴ ┴ └────────┘ ┴ └─────────┘ ┴ └─
typ ─────┘└───────────┘┴┴┴ ┴ ┴ └────────┘ ┴ └─────────┘ ┴ └─
doc ─────┘└───────────┘┴ ┴ ┴ ┴ └────────┘ ┴ └─────────┘ ┴ └─
txt ─────┘ ┴ ┴ ┴ ┴ └────────┘ ┴ └─────────┘ ┴ └─
par ─────┘ ┴ ┴ ┴ ┴ └────────┘ ┴ └─────────┘ ┴ └─
pid ─────┘ ┴ ┴ ┴ ┴ └────────┘ ┴ └─────────┘ ┴ └─
st ────────────────────────────────────────────────────────────────────────
323 (I.inv_fun ⁻¹' (i.1.symm.trans j.1).source ∩ range I.to_fun) x,
id └───────┘ ┴ ┴ └───┘ └──────┘
src ───────────┘ └───────┘┴ ┴ └────────────┘ └─────────┘ ┴└───┘┴└──────┘└┘
typ ───────────┘ └───────┘┴ ┴ ┴└────────────┘┴└─────────┘ ┴└───┘┴└──────┘└┘
doc ───────────┘ ┴ ┴ └────────────┘ └─────────┘ ┴└───┘┴ └┘
txt ───────────┘ ┴ ┴ └────────────┘ └─────────┘ ┴ ┴ └┘
par ───────────┘ ┴ ┴ └────────────┘ └─────────┘ ┴ ┴ └┘
pid ───────────┘ ┴ ┴ └────────────┘ └─────────┘ ┴ ┴ └┘
st ─────────────────────────────────────────────────────────────────────────┘└─
324 { assume x hx,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ─────┘└─────────┘└─
325 have N : I.inv_fun ⁻¹' (i.1.symm.trans j.1).source ∈ nhds x :=
id └───────┘ ┴ ┴ └──┘ ┴
src └───────┘└───────┘┴ ┴ └────────────┘ └─────────┘ ┴└──┘┴ └───
typ └───────┘└───────┘┴ ┴ ┴└────────────┘┴└─────────┘ ┴└──┘┴┴└───
doc └───────┘ ┴ ┴ └────────────┘ └─────────┘ ┴└──┘┴ └───
txt └───────┘ ┴ ┴ └────────────┘ └─────────┘ ┴ ┴ └───
par └───────┘ ┴ ┴ └────────────┘ └─────────┘ ┴ ┴ └───
pid └────┘└─┘ ┴ ┴ └────────────┘ └─────────┘ ┴ ┴ └───
st ─────────────────────────────────────────────────────────────────────
326 I.continuous_inv_fun.continuous_at.preimage_mem_nhds
id └──────────────────────────────────────────────────┘
src ───────┘└──────────────────────────────────────────────────┘└
typ ───────┘└──────────────────────────────────────────────────┘└
doc ───────┘ └
txt ───────┘ └
par ───────┘ └
pid ───────┘ └
st ─────────────────────────────────────────────────────────────
327 (mem_nhds_sets (local_homeomorph.open_source _) hx.1),
id └───────────┘ └──────────────────────────┘ └┘
src ─────────┘ └───────────┘┴ └──────────────────────────┘└──┘ └─┘
typ ─────────┘ └───────────┘┴ └──────────────────────────┘└──┘└┘└─┘
doc ─────────┘ ┴ └──┘ └─┘
txt ─────────┘ ┴ └──┘ └─┘
par ─────────┘ ┴ └──┘ └─┘
pid ─────────┘ ┴ └──┘ └─┘
st ──────────────────────────────────────────────────────────────┘└─
328 symmetry,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
st ─────────────┘└─
329 rw inter_comm,
id └────────┘
src └─┘└────────┘
typ └─┘└────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ──────────────────┘└─
330 exact fderiv_within_inter N (I.unique_diff _ hx.2) },
id └─────────────────┘ ┴ └───────────┘ └┘
src └────┘└─────────────────┘┴ ┴ └───────────┘└─┘ └──┘
typ └────┘└─────────────────┘┴┴┴ └───────────┘└─┘└┘└──┘
doc └────┘ ┴ ┴ └─┘ └──┘
txt └────┘ ┴ ┴ └─┘ └──┘
par └────┘ ┴ ┴ └─┘ └──┘
pid ┴ ┴ ┴ └─┘ └─┘┴
st ────────────────────────────────────────────────────────┘└┘└
331 apply times_cont_diff_on.congr C (unique_diff_on.prod B unique_diff_on_univ),
id └──────────────────────┘ ┴ └─────────────────┘ ┴ └─────────────────┘
src └────┘└──────────────────────┘┴ ┴ └─────────────────┘┴ ┴└─────────────────┘┴
typ └────┘└──────────────────────┘┴┴┴ └─────────────────┘┴┴┴└─────────────────┘┴
doc └────┘ ┴ ┴ └─────────────────┘┴ ┴ ┴
txt └────┘ ┴ ┴ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴ ┴
st ───────────────────────────────────────────────────────────────────────────────┘└─
332 rintros ⟨x, v⟩ hx,
src └───────────────┘
typ └───────────────┘
doc └───────────────┘
txt └───────────────┘
par └───────────────┘
pid └────────┘
st ────────────────────┘
333 have E : x ∈ I.inv_fun ⁻¹' (i.1.symm.trans j.1).source ∩ range I.to_fun,
334 by simpa using hx,
id └┘
src └──────────┘
typ └──────────┘└┘
doc └──────────┘
txt └──────────┘
par └──────────┘
pid ┴└────┘
335 have : I.to_fun (I.inv_fun x) = x, by simp [E.2],
id ┴
src └────┘ └─┘
typ └────┘┴└─┘
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴┴ └─┘
336 dsimp,
337 rw [this, D x E],
338 refl
339 end,
st └─┘
340 coord_change_self := λi x hx v, begin
id ┴ ┴ └┘ ┴
typ ┴ ┴ └┘ ┴
st └─────
341 /- Locally, a self-change of coordinate is just the identity, thus its derivative is the
st ─────────────────────────────────────────────────────────────────────────────────────────────
342 identity. One just needs to write this carefully, paying attention to the sets where the
st ─────────────────────────────────────────────────────────────────────────────────────────────
343 functions are defined. -/
st ──────────────────────────────
344 have A : I.inv_fun ⁻¹' (i.1.symm.trans i.1).source ∩ range I.to_fun ∈
id └───────┘ └─┘ ┴ ┴ ┴
src └───────┘└───────┘┴└─┘┴ └────────────┘ └─────────┘┴┴ ┴ ┴┴└
typ └───────┘└───────┘┴└─┘┴ └────────────┘┴└─────────┘┴┴ ┴ ┴┴└
doc └───────┘ ┴└─┘┴ └────────────┘ └─────────┘ ┴ ┴ ┴ └
txt └───────┘ ┴ ┴ └────────────┘ └─────────┘ ┴ ┴ ┴ └
par └───────┘ ┴ ┴ └────────────┘ └─────────┘ ┴ ┴ ┴ └
pid └────┘└─┘ ┴ ┴ └────────────┘ └─────────┘ ┴ ┴ ┴ └
st ──────────────────────────────────────────────────────────────────────────
345 nhds_within (I.to_fun x) (range I.to_fun),
id └─────────┘ ┴ └───┘ └──────┘
src ─────┘└─────────┘┴ ┴ └┘ └───┘┴└──────┘┴
typ ─────┘└─────────┘┴ ┴┴└┘ └───┘┴└──────┘┴
doc ─────┘└─────────┘┴ ┴ └┘ └───┘┴ ┴
txt ─────┘ ┴ ┴ └┘ ┴ ┴
par ─────┘ ┴ ┴ └┘ ┴ ┴
pid ─────┘ ┴ ┴ └┘ ┴ ┴
st ──────────────────────────────────────────────┘└─
346 { rw inter_comm,
id └────────┘
src └─┘└────────┘
typ └─┘└────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ────┘ └───────────┘ └
347 apply inter_mem_nhds_within,
id └───────────────────┘
src └────┘└───────────────────┘
typ └────┘└───────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ────────────────────────────────┘└─
348 apply I.continuous_inv_fun.continuous_at.preimage_mem_nhds
id └──────────────────────────────────────────────────┘
src └────┘└──────────────────────────────────────────────────┘└
typ └────┘└──────────────────────────────────────────────────┘└
doc └────┘ └
txt └────┘ └
par └────┘ └
pid ┴ └
st ─────────────────────────────────────────────────────────────────
349 (mem_nhds_sets (local_homeomorph.open_source _) _),
id └───────────┘ └──────────────────────────┘
src ───────┘ └───────────┘┴ └──────────────────────────┘└────┘
typ ───────┘ └───────────┘┴ └──────────────────────────┘└────┘
doc ───────┘ ┴ └────┘
txt ───────┘ ┴ └────┘
par ───────┘ ┴ └────┘
pid ───────┘ ┴ └────┘
st ─────────────────────────────────────────────────────────┘└┘
350 simp [hx, local_equiv.trans_source, i.1.map_target] },
st └┘
351 have B : ∀ᶠ y in nhds_within (I.to_fun x) (range I.to_fun),
id ┴ ┴
typ ┴ ┴
352 (I.to_fun ∘ i.1.to_fun ∘ i.1.inv_fun ∘ I.inv_fun) y = (id : E → E) y,
id ┴
typ ┴
353 { apply filter.mem_sets_of_superset A,
354 assume y hy,
355 rw ← model_with_corners.image at hy,
356 rcases hy with ⟨z, hz⟩,
357 simp [local_equiv.trans_source] at hz,
358 simp [hz.2.symm, hz.1] },
st └┘
359 have C : fderiv_within 𝕜 (I.to_fun ∘ i.1.to_fun ∘ i.1.inv_fun ∘ I.inv_fun)
360 (range I.to_fun) (I.to_fun x) =
361 fderiv_within 𝕜 (id : E → E) (range I.to_fun) (I.to_fun x) :=
id ┴ ┴ ┴
typ ┴ ┴ ┴
362 fderiv_within_congr_of_mem_nhds_within (I.unique_diff _ (mem_range_self _)) B (by simp [hx]),
363 rw fderiv_within_id (I.unique_diff _ (mem_range_self _)) at C,
364 rw C,
365 refl
366 end,
st └─┘
367 coord_change_comp := λi j u x hx, begin
id ┴
typ ┴
368 /- The cocycle property is just the fact that the derivative of a composition is the product of
369 the derivatives. One needs however to check that all the functions one considers are smooth, and
370 to pay attention to the domains where these functions are defined, making this proof a little
371 bit cumbersome although there is nothing complicated here. -/
372 have M : I.to_fun x ∈
id ┴
typ ┴
373 (I.inv_fun ⁻¹' ((i.1.symm.trans j.1).trans (j.1.symm.trans u.1)).source ∩ range I.to_fun) :=
374 ⟨by simpa using hx, mem_range_self _⟩,
375 have U : unique_diff_within_at 𝕜
id ┴
typ ┴
376 (I.inv_fun ⁻¹' ((i.1.symm.trans j.1).trans (j.1.symm.trans u.1)).source ∩ range I.to_fun)
377 (I.to_fun x),
id ┴
typ ┴
378 { have : unique_diff_on 𝕜
id ┴
typ ┴
379 (I.inv_fun ⁻¹' ((i.1.symm.trans j.1).trans (j.1.symm.trans u.1)).source ∩ range I.to_fun),
380 { rw inter_comm,
381 exact I.unique_diff.inter (I.continuous_inv_fun _ (local_homeomorph.open_source _)) },
st └┘
382 exact this _ M },
st └┘
383 have A : fderiv_within 𝕜 ((I.to_fun ∘ u.1.to_fun ∘ j.1.inv_fun ∘ I.inv_fun)
384 ∘ (I.to_fun ∘ j.1.to_fun ∘ i.1.inv_fun ∘ I.inv_fun))
385 (I.inv_fun ⁻¹' ((i.1.symm.trans j.1).trans (j.1.symm.trans u.1)).source ∩ range I.to_fun)
386 (I.to_fun x)
387 = (fderiv_within 𝕜 (I.to_fun ∘ u.1.to_fun ∘ j.1.inv_fun ∘ I.inv_fun)
388 (I.inv_fun ⁻¹' (j.1.symm.trans u.1).source ∩ range I.to_fun)
389 ((I.to_fun ∘ j.1.to_fun ∘ i.1.inv_fun ∘ I.inv_fun) (I.to_fun x))).comp
390 (fderiv_within 𝕜 (I.to_fun ∘ j.1.to_fun ∘ i.1.inv_fun ∘ I.inv_fun)
id ┴
typ ┴
391 (I.inv_fun ⁻¹' ((i.1.symm.trans j.1).trans (j.1.symm.trans u.1)).source ∩ range I.to_fun)
392 (I.to_fun x)),
id ┴
typ ┴
393 { apply fderiv_within.comp _ _ _ _ U,
394 show differentiable_within_at 𝕜 (I.to_fun ∘ j.1.to_fun ∘ i.1.inv_fun ∘ I.inv_fun)
id ┴
typ ┴
395 (I.inv_fun ⁻¹' ((i.1.symm.trans j.1).trans (j.1.symm.trans u.1)).source ∩ range I.to_fun)
396 (I.to_fun x),
id ┴
typ ┴
397 { have A : times_cont_diff_on 𝕜 ⊤
id ┴
typ ┴
398 (I.to_fun ∘ (i.1.symm.trans j.1).to_fun ∘ I.inv_fun)
399 (I.inv_fun ⁻¹' (i.1.symm.trans j.1).source ∩ range I.to_fun) :=
400 (has_groupoid.compatible (times_cont_diff_groupoid ⊤ I) i.2 j.2).1,
401 have B : differentiable_on 𝕜 (I.to_fun ∘ j.1.to_fun ∘ i.1.inv_fun ∘ I.inv_fun)
id ┴
typ ┴
402 (I.inv_fun ⁻¹' ((i.1.symm.trans j.1).trans (j.1.symm.trans u.1)).source ∩ range I.to_fun),
403 { apply (A.differentiable_on (lattice.le_top)).mono,
404 have : ((i.1.symm.trans j.1).trans (j.1.symm.trans u.1)).source ⊆ (i.1.symm.trans j.1).source :=
405 inter_subset_left _ _,
406 exact inter_subset_inter (preimage_mono this) (subset.refl (range I.to_fun)) },
st └┘
407 apply B,
408 simpa [mem_inter_iff, -mem_image, -mem_range, mem_range_self] using hx },
st └┘
409 show differentiable_within_at 𝕜 (I.to_fun ∘ u.1.to_fun ∘ j.1.inv_fun ∘ I.inv_fun)
id ┴
typ ┴
410 (I.inv_fun ⁻¹' (j.1.symm.trans u.1).source ∩ range I.to_fun)
411 ((I.to_fun ∘ j.1.to_fun ∘ i.1.inv_fun ∘ I.inv_fun) (I.to_fun x)),
id ┴
typ ┴
412 { have A : times_cont_diff_on 𝕜 ⊤
id ┴
typ ┴
413 (I.to_fun ∘ (j.1.symm.trans u.1).to_fun ∘ I.inv_fun)
414 (I.inv_fun ⁻¹' (j.1.symm.trans u.1).source ∩ range I.to_fun) :=
415 (has_groupoid.compatible (times_cont_diff_groupoid ⊤ I) j.2 u.2).1,
416 apply A.differentiable_on (lattice.le_top),
417 rw [local_homeomorph.trans_source] at hx,
418 simp [mem_inter_iff, -mem_image, -mem_range, mem_range_self],
419 exact hx.2 },
st └┘
420 show (I.inv_fun ⁻¹' ((i.1.symm.trans j.1).trans (j.1.symm.trans u.1)).source ∩ range I.to_fun)
421 ⊆ (I.to_fun ∘ j.1.to_fun ∘ i.1.inv_fun ∘ I.inv_fun) ⁻¹'
422 (I.inv_fun ⁻¹' (j.1.symm.trans u.1).source ∩ range I.to_fun),
423 { assume y hy,
424 simp [-mem_range, local_equiv.trans_source] at hy,
425 rw [local_equiv.left_inv] at hy,
426 { simp [-mem_range, mem_range_self, hy, local_equiv.trans_source] },
st └┘
427 { exact hy.1.1.2 } } },
st └────┘
428 have B : fderiv_within 𝕜 ((I.to_fun ∘ u.1.to_fun ∘ j.1.inv_fun ∘ I.inv_fun)
429 ∘ (I.to_fun ∘ j.1.to_fun ∘ i.1.inv_fun ∘ I.inv_fun))
430 (I.inv_fun ⁻¹' ((i.1.symm.trans j.1).trans (j.1.symm.trans u.1)).source ∩ range I.to_fun)
431 (I.to_fun x)
432 = fderiv_within 𝕜 (I.to_fun ∘ u.1.to_fun ∘ i.1.inv_fun ∘ I.inv_fun)
id ┴
typ ┴
433 (I.inv_fun ⁻¹' ((i.1.symm.trans j.1).trans (j.1.symm.trans u.1)).source ∩ range I.to_fun)
434 (I.to_fun x),
id ┴
typ ┴
435 { have E : ∀ y ∈ (I.inv_fun ⁻¹' ((i.1.symm.trans j.1).trans (j.1.symm.trans u.1)).source ∩ range I.to_fun),
436 ((I.to_fun ∘ u.1.to_fun ∘ j.1.inv_fun ∘ I.inv_fun)
437 ∘ (I.to_fun ∘ j.1.to_fun ∘ i.1.inv_fun ∘ I.inv_fun)) y =
438 (I.to_fun ∘ u.1.to_fun ∘ i.1.inv_fun ∘ I.inv_fun) y,
439 { assume y hy,
440 simp only [function.comp_app, model_with_corners_left_inv],
441 rw [j.1.left_inv],
442 exact hy.1.1.2 },
st └┘
443 exact fderiv_within_congr U E (E _ M) },
st └┘
444 have C : fderiv_within 𝕜 (I.to_fun ∘ u.1.to_fun ∘ i.1.inv_fun ∘ I.inv_fun)
445 (I.inv_fun ⁻¹' ((i.1.symm.trans j.1).trans (j.1.symm.trans u.1)).source ∩ range I.to_fun)
446 (I.to_fun x) =
447 fderiv_within 𝕜 (I.to_fun ∘ u.1.to_fun ∘ i.1.inv_fun ∘ I.inv_fun)
id ┴
typ ┴
448 (range I.to_fun) (I.to_fun x),
id ┴
typ ┴
449 { rw inter_comm,
450 apply fderiv_within_inter _ (I.unique_diff _ (mem_range_self _)),
451 apply I.continuous_inv_fun.continuous_at.preimage_mem_nhds
452 (mem_nhds_sets (local_homeomorph.open_source _) _),
453 simpa using hx },
st └┘
454 have D : fderiv_within 𝕜 (I.to_fun ∘ u.1.to_fun ∘ j.1.inv_fun ∘ I.inv_fun)
455 (I.inv_fun ⁻¹' (j.1.symm.trans u.1).source ∩ range I.to_fun)
456 ((I.to_fun ∘ j.1.to_fun ∘ i.1.inv_fun ∘ I.inv_fun) (I.to_fun x)) =
457 fderiv_within 𝕜 (I.to_fun ∘ u.1.to_fun ∘ j.1.inv_fun ∘ I.inv_fun)
id ┴
typ ┴
458 (range I.to_fun)
459 ((I.to_fun ∘ j.1.to_fun ∘ i.1.inv_fun ∘ I.inv_fun) (I.to_fun x)),
id ┴
typ ┴
460 { rw inter_comm,
461 apply fderiv_within_inter _ (I.unique_diff _ (mem_range_self _)),
462 apply I.continuous_inv_fun.continuous_at.preimage_mem_nhds
463 (mem_nhds_sets (local_homeomorph.open_source _) _),
464 rw [local_homeomorph.trans_source] at hx,
465 simp [mem_inter_iff, -mem_image, -mem_range, mem_range_self],
466 exact hx.2 },
st └┘
467 have E : fderiv_within 𝕜 (I.to_fun ∘ j.1.to_fun ∘ i.1.inv_fun ∘ I.inv_fun)
468 (I.inv_fun ⁻¹' ((i.1.symm.trans j.1).trans (j.1.symm.trans u.1)).source ∩ range I.to_fun)
469 (I.to_fun x) =
470 (fderiv_within 𝕜 (I.to_fun ∘ j.1.to_fun ∘ i.1.inv_fun ∘ I.inv_fun)
id ┴
typ ┴
471 (range I.to_fun)
472 (I.to_fun x)),
id ┴
typ ┴
473 { rw inter_comm,
474 apply fderiv_within_inter _ (I.unique_diff _ (mem_range_self _)),
475 apply I.continuous_inv_fun.continuous_at.preimage_mem_nhds
476 (mem_nhds_sets (local_homeomorph.open_source _) _),
477 simpa using hx },
st └┘
478 rw [B, C, D, E] at A,
479 rw A,
480 assume v,
481 simp,
482 unfold_coes,
483 simp
484 end }
st └─┘
485
486 /-- The tangent bundle to a smooth manifold, as a plain type. -/
487 def tangent_bundle := (tangent_bundle_core I M).to_topological_fiber_bundle_core.total_space
id ┴
typ ┴
488
489 /-- The projection from the tangent bundle of a smooth manifold to the manifold. As the tangent
490 bundle is represented internally as a product type, the notation `p.1` also works for the projection
491 of the point `p`. -/
492 def tangent_bundle.proj : tangent_bundle I M → M :=
id ┴ ┴
typ ┴ ┴
493 (tangent_bundle_core I M).to_topological_fiber_bundle_core.proj
id ┴
typ ┴
494
495 variable {M}
496
497 /-- The tangent space at a point of the manifold `M`. It is just `E`. -/
498 def tangent_space (x : M) : Type* :=
id ┴
typ ┴
499 (tangent_bundle_core I M).to_topological_fiber_bundle_core.fiber x
id ┴ ┴
typ ┴ ┴
500
501 section tangent_bundle_instances
502
503 /- In general, the definition of tangent_bundle and tangent_space are not reducible, so that type
504 class inference does not pick wrong instances. In this section, we record the right instances for
505 them, noting in particular that the tangent bundle is a smooth manifold. -/
506 variable (M)
507 local attribute [reducible] tangent_bundle
doc └───────┘
508
509 instance : topological_space (tangent_bundle I M) := by apply_instance
id ┴
typ ┴
510 instance : manifold (H × E) (tangent_bundle I M) := by apply_instance
id ┴ ┴ ┴
typ ┴ ┴ ┴
511 instance : smooth_manifold_with_corners I.tangent (tangent_bundle I M) := by apply_instance
id ┴
typ ┴
512
513 local attribute [reducible] tangent_space topological_fiber_bundle_core.fiber
doc └───────┘
514 /- When `topological_fiber_bundle_core.fiber` is reducible, then
515 `topological_fiber_bundle_core.topological_space_fiber` can be applied to prove that any space is
516 a topological space, with several unknown metavariables. This is a bad instance, that we disable.-/
517 local attribute [instance, priority 0] topological_fiber_bundle_core.topological_space_fiber
518
519 variables {M} (x : M)
520
521 instance : topological_module 𝕜 (tangent_space I x) := by apply_instance
id ┴ ┴
typ ┴ ┴
522 instance : topological_space (tangent_space I x) := by apply_instance
id └┘ └┘ └┘ └┘ ┴ ┴
src └┘ └┘ └┘ └┘ ┴
typ └┘ └┘ └┘ └┘ ┴ ┴
doc └┘ └┘ └┘ └┘ ┴
523 instance : add_comm_group (tangent_space I x) := by apply_instance
id └┘ └┘ └┘ └┘ ┴
src └┘ └┘ └┘ └┘
typ └┘ └┘ └┘ └┘ ┴
524 instance : topological_add_group (tangent_space I x) := by apply_instance
id ┴
typ ┴
525 instance : vector_space 𝕜 (tangent_space I x) := by apply_instance
id ┴ ┴
typ ┴ ┴
526
527 end tangent_bundle_instances
528
529 variable (M)
530
531 /-- The tangent bundle projection on the basis is a continuous map. -/
532 lemma tangent_bundle_proj_continuous : continuous (tangent_bundle.proj I M) :=
id ┴
typ ┴
533 topological_fiber_bundle_core.continuous_proj _
534
535 /-- The tangent bundle projection on the basis is an open map. -/
536 lemma tangent_bundle_proj_open : is_open_map (tangent_bundle.proj I M) :=
id ┴
typ ┴
537 topological_fiber_bundle_core.is_open_map_proj _
538
539 /-- In the tangent bundle to the model space, the charts are just the identity-/
540 @[simp] lemma tangent_bundle_model_space_chart_at (p : tangent_bundle I H) :
id ┴
typ ┴
doc └──┘
541 (chart_at (H × E) p).to_local_equiv = local_equiv.refl (H × E) :=
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
542 begin
543 have A : ∀ x_fst, fderiv_within 𝕜 (I.to_fun ∘ I.inv_fun) (range I.to_fun) (I.to_fun x_fst)
id └───┘ ┴
typ └───┘ ┴
544 = continuous_linear_map.id,
545 { assume x_fst,
546 have : fderiv_within 𝕜 (I.to_fun ∘ I.inv_fun) (range I.to_fun) (I.to_fun x_fst)
547 = fderiv_within 𝕜 id (range I.to_fun) (I.to_fun x_fst),
id ┴ └───┘
typ ┴ └───┘
548 { refine fderiv_within_congr (I.unique_diff _ (mem_range_self _)) (λy hy, _) (by simp),
id ┴
typ ┴
549 exact model_with_corners_right_inv _ hy },
st └┘
550 rwa fderiv_within_id (I.unique_diff _ (mem_range_self _)) at this },
st └┘
551 ext x : 1,
552 show (chart_at (H × E) p).to_fun x = (local_equiv.refl (H × E)).to_fun x,
id ┴ ┴
typ ┴ ┴
553 { cases x,
554 simp [chart_at, manifold.chart_at, basic_smooth_bundle_core.chart,
555 topological_fiber_bundle_core.local_triv, topological_fiber_bundle_core.local_triv',
556 basic_smooth_bundle_core.to_topological_fiber_bundle_core, tangent_bundle_core],
557 erw [local_equiv.refl_to_fun, local_equiv.refl_inv_fun, A],
558 refl },
st └┘
559 show ∀ x, ((chart_at (H × E) p).to_local_equiv).inv_fun x = (local_equiv.refl (H × E)).inv_fun x,
id ┴ ┴ ┴
typ ┴ ┴ ┴
560 { rintros ⟨x_fst, x_snd⟩,
561 simp [chart_at, manifold.chart_at, basic_smooth_bundle_core.chart,
562 topological_fiber_bundle_core.local_triv, topological_fiber_bundle_core.local_triv',
563 basic_smooth_bundle_core.to_topological_fiber_bundle_core, tangent_bundle_core],
564 erw [local_equiv.refl_to_fun, local_equiv.refl_inv_fun, A],
565 refl },
st └┘
566 show ((chart_at (H × E) p).to_local_equiv).source = (local_equiv.refl (H × E)).source,
id ┴ ┴
typ ┴ ┴
567 by simp [chart_at, manifold.chart_at, basic_smooth_bundle_core.chart,
568 topological_fiber_bundle_core.local_triv, topological_fiber_bundle_core.local_triv',
569 basic_smooth_bundle_core.to_topological_fiber_bundle_core, tangent_bundle_core,
570 local_equiv.trans_source]
571 end
st └─┘
572
573 variable (H)
574 /-- In the tangent bundle to the model space, the topology is the product topology, i.e., the bundle
575 is trivial -/
576 lemma tangent_bundle_model_space_topology_eq_prod :
577 tangent_bundle.topological_space I H = prod.topological_space :=
id ┴
typ ┴
578 begin
579 ext o,
580 let x : tangent_bundle I H := (I.inv_fun (0 : E), (0 : E)),
id ┴ ┴
typ ┴ ┴
581 let e := chart_at (H × E) x,
id ┴ ┴
typ ┴ ┴
582 have e_source : e.source = univ, by { simp [e], refl },
st └┘
583 have e_target : e.target = univ, by { simp [e], refl },
st └┘
584 let e' := e.to_homeomorph_of_source_eq_univ_target_eq_univ e_source e_target,
585 split,
586 { assume ho,
587 have := e'.continuous_inv_fun o ho,
588 simpa [e', tangent_bundle_model_space_chart_at] },
st └┘
589 { assume ho,
590 have := e'.continuous_to_fun o ho,
591 simpa [e', tangent_bundle_model_space_chart_at] }
st └─
592 end
st ──┘
593
594 end tangent_bundle